1  /-
  2  Copyright (c) 2015 Jeremy Avigad. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Jeremy Avigad, Robert Y. Lewis
  5  
  6  The power operation on monoids and groups. We separate this from group, because it depends on
  7  nat, which in turn depends on other parts of algebra.
  8  
  9  We have "pow a n" for natural number powers, and "gpow a i" for integer powers. The notation
 10  a^n is used for the first, but users can locally redefine it to gpow when needed.
 11  
 12  Note: power adopts the convention that 0^0=1.
 13  -/
 14  import algebra.group
src         └───────────┘
 15  import data.int.basic data.list.basic
src         └────────────┘ └─────────────┘
 16  
 17  universes u v
 18  variable {α : Type u}
 19  
 20  /-- The power operation in a monoid. `a^n = a*a*...*a` n times. -/
 21  def monoid.pow [monoid α] (a : α) : ℕ → α
id                   └────┘              
src                  └────┘              
typ                  └────┘              
 22  | 0     := 1
 23  | (n+1) := a * monoid.pow n
id              └────────┘
src              
typ             └────────┘
 24  
 25  def add_monoid.smul [add_monoid α] (n : ℕ) (a : α) : α :=
id                        └────────┘                   
src                       └────────┘         
typ                       └────────┘                   
 26  @monoid.pow (multiplicative α) _ a n
id    └────────┘  └────────────┘      
src   └────────┘  └────────────┘
typ   └────────┘  └────────────┘      
doc   └────────┘
 27  
 28  precedence `•`:70
 29  localized "infix ` • ` := add_monoid.smul" in add_monoid
 30  
 31  @[priority 5] instance monoid.has_pow [monoid α] : has_pow α ℕ := ⟨monoid.pow⟩
id                                          └────┘     └─────┘       └────────┘
src                                         └────┘      └─────┘        └────────┘
typ                                         └────┘     └─────┘       └────────┘
doc                                                                     └────────┘
 32  
 33   /- monoid -/
 34  section monoid
 35  variables [monoid α] {β : Type u} [add_monoid β]
id              └────┘                  └────────┘
src             └────┘                  └────────┘
typ             └────┘                  └────────┘
 36  
 37  @[simp] theorem pow_zero (a : α) : a^0 = 1 := rfl
id                                             └─┘
src                                              └─┘
typ                                            └─┘
doc    └──┘
 38  @[simp] theorem add_monoid.zero_smul (a : β) : 0 • a = 0 := rfl
id                                                           └─┘
src                                                            └─┘
typ                                                          └─┘
doc    └──┘
 39  
 40  theorem pow_succ (a : α) (n : ℕ) : a^(n+1) = a * a^n := rfl
id                                               └─┘
src                                                    └─┘
typ                                              └─┘
 41  theorem succ_smul (a : β) (n : ℕ) : (n+1)•a = a + n•a := rfl
id                                                └─┘
src                                                     └─┘
typ                                               └─┘
 42  
 43  @[simp] theorem pow_one (a : α) : a^1 = a := mul_one _
id                                           └─────┘
src                                             └─────┘
typ                                          └─────┘
doc    └──┘
 44  @[simp] theorem add_monoid.one_smul (a : β) : 1•a = a := add_zero _
id                                                       └──────┘
src                                                         └──────┘
typ                                                      └──────┘
doc    └──┘
 45  
 46  theorem pow_mul_comm' (a : α) (n : ℕ) : a^n * a = a * a^n :=
id                                               
src                                                    
typ                                              
 47  by induction n with n ih; [rw [pow_zero, one_mul, mul_one],
id                                └──────┘  └─────┘  └─────┘
src     └────────┘ └────────┘  └──┘└──────┘└┘└─────┘└┘└─────┘
typ     └────────┘└────────┘  └──┘└──────┘└┘└─────┘└┘└─────┘
doc     └────────┘ └────────┘   └──┘        └┘       └┘       
txt     └────────┘ └────────┘   └──┘        └┘       └┘       
par     └────────┘ └────────┘   └──┘        └┘       └┘       
pid               └───────┘     └┘        └┘       └┘       
st     └───────────────────────────┘└──────┘└───────┘└───────┘└─
 48    rw [pow_succ, mul_assoc, ih]]
id         └──────┘  └───────┘  └┘
src    └──┘└──────┘└┘└───────┘└┘  
typ    └──┘└──────┘└┘└───────┘└┘└┘
doc    └──┘        └┘         └┘  
txt    └──┘        └┘         └┘  
par    └──┘        └┘         └┘  
pid      └┘        └┘         └┘  
st   ─────┘└──────┘└─────────┘└──┘
 49  theorem smul_add_comm' : ∀ (a : β) (n : ℕ), n•a + a = a + n•a :=
id                                                   
src                                                        
typ                                                  
 50  @pow_mul_comm' (multiplicative β) _
id    └───────────┘  └────────────┘ 
src   └───────────┘  └────────────┘
typ   └───────────┘  └────────────┘ 
 51  
 52  theorem pow_succ' (a : α) (n : ℕ) : a^(n+1) = a^n * a :=
id                                            
src                                               
typ                                           
 53  by rw [pow_succ, pow_mul_comm']
id          └──────┘  └───────────┘
src     └──┘└──────┘└┘└───────────┘└┘
typ     └──┘└──────┘└┘└───────────┘└┘
doc     └──┘        └┘             └┘
txt     └──┘        └┘             └┘
par     └──┘        └┘             └┘
pid       └┘        └┘             
st     └───────────┘└─────────────┘
 54  theorem succ_smul' (a : β) (n : ℕ) : (n+1)•a = n•a + a :=
id                                             
src                                                
typ                                            
 55  by rw [succ_smul, smul_add_comm']
id          └───────┘  └────────────┘
src     └──┘└───────┘└┘└────────────┘└─
typ     └──┘└───────┘└┘└────────────┘└─
doc     └──┘         └┘              └─
txt     └──┘         └┘              └─
par     └──┘         └┘              └─
pid       └┘         └┘              
st     └────────────┘└──────────────┘
 56  
src  
typ  
doc  
txt  
par  
pid  
st   
 57  theorem pow_two (a : α) : a^2 = a * a :=
id                                 
src                                  
typ                                
 58  show a*(a*1)=a*a, by rw mul_one
id                   └─────┘
src                   └─┘└─────┘
typ               └─┘└─────┘
doc                       └─┘       
txt                       └─┘       
par                       └─┘       
pid                                
st                       └──────────┘
 59  theorem two_smul (a : β) : 2•a = a + a :=
id                                  
src                                   
typ                                 
 60  show a+(a+0)=a+a, by rw add_zero
id                   └──────┘
src                   └─┘└──────┘
typ               └─┘└──────┘
doc                       └─┘        
txt                       └─┘        
par                       └─┘        
pid                                 
st                       └────────────
 61  
src  
typ  
doc  
txt  
par  
pid  
st   
 62  theorem pow_add (a : α) (m n : ℕ) : a^(m + n) = a^m * a^n :=
id                                             
src                                                   
typ                                            
 63  by induction n with n ih; [rw [add_zero, pow_zero, mul_one],
id                                └──────┘  └──────┘  └─────┘
src     └────────┘ └────────┘  └──┘└──────┘└┘└──────┘└┘└─────┘
typ     └────────┘└────────┘  └──┘└──────┘└┘└──────┘└┘└─────┘
doc     └────────┘ └────────┘   └──┘        └┘        └┘       
txt     └────────┘ └────────┘   └──┘        └┘        └┘       
par     └────────┘ └────────┘   └──┘        └┘        └┘       
pid               └───────┘     └┘        └┘        └┘       
st     └───────────────────────────┘└──────┘└────────┘└───────┘└─
 64    rw [pow_succ, ← pow_mul_comm', ← mul_assoc, ← ih, ← pow_succ']]; refl
id         └──────┘    └───────────┘    └───────┘    └┘    └───────┘
src    └──┘└──────┘└──┘└───────────┘└──┘└───────┘└──┘  └──┘└───────┘   └───┘
typ    └──┘└──────┘└──┘└───────────┘└──┘└───────┘└──┘└┘└──┘└───────┘   └───┘
doc    └──┘        └──┘             └──┘         └──┘  └──┘            └───┘
txt    └──┘        └──┘             └──┘         └──┘  └──┘            └───┘
par    └──┘        └──┘             └──┘         └──┘  └──┘            └───┘
pid      └┘        └──┘             └──┘         └──┘  └──┘                
st   ─────┘└──────┘└───────────────┘└───────────┘└────┘└───────────┘└──────┘
 65  theorem add_monoid.add_smul : ∀ (a : β) (m n : ℕ), (m + n)•a = m•a + n•a :=
id                                                            
src                                                                  
typ                                                           
 66  @pow_add (multiplicative β) _
id    └─────┘  └────────────┘ 
src   └─────┘  └────────────┘
typ   └─────┘  └────────────┘ 
 67  
 68  @[simp] theorem one_pow (n : ℕ) : (1 : α)^n = (1:α) :=
id                                               
src                                            
typ                                              
doc    └──┘
 69  by induction n with n ih; [refl, rw [pow_succ, ih, one_mul]]
id                                      └──────┘  └┘  └─────┘
src     └────────┘ └────────┘  └──┘  └──┘└──────┘└┘  └┘└─────┘
typ     └────────┘└────────┘  └──┘  └──┘└──────┘└┘└┘└┘└─────┘
doc     └────────┘ └────────┘   └──┘  └──┘        └┘  └┘       
txt     └────────┘ └────────┘   └──┘  └──┘        └┘  └┘       
par     └────────┘ └────────┘   └──┘  └──┘        └┘  └┘       
pid               └───────┘           └┘        └┘  └┘       
st     └─────────────────────────────────┘└──────┘└──┘└───────┘
 70  @[simp] theorem add_monoid.smul_zero (n : ℕ) : n•(0 : β) = (0:β) :=
id                                                            
src                                                         
typ                                                           
doc    └──┘
 71  by induction n with n ih; [refl, rw [succ_smul, ih, zero_add]]
id                                      └───────┘  └┘  └──────┘
src     └────────┘ └────────┘  └──┘  └──┘└───────┘└┘  └┘└──────┘
typ     └────────┘└────────┘  └──┘  └──┘└───────┘└┘└┘└┘└──────┘
doc     └────────┘ └────────┘   └──┘  └──┘         └┘  └┘        
txt     └────────┘ └────────┘   └──┘  └──┘         └┘  └┘        
par     └────────┘ └────────┘   └──┘  └──┘         └┘  └┘        
pid               └───────┘           └┘         └┘  └┘        
st     └─────────────────────────────────┘└───────┘└──┘└────────┘
 72  
 73  theorem pow_mul (a : α) (m n : ℕ) : a^(m * n) = (a^m)^n :=
id                                             
src                                                  
typ                                            
 74  by induction n with n ih; [rw mul_zero, rw [nat.mul_succ, pow_add, pow_succ', ih]]; refl
id                               └──────┘      └──────────┘  └─────┘  └───────┘  └┘
src     └────────┘ └────────┘  └─┘└──────┘  └──┘└──────────┘└┘└─────┘└┘└───────┘└┘     └───┘
typ     └────────┘└────────┘  └─┘└──────┘  └──┘└──────────┘└┘└─────┘└┘└───────┘└┘└┘   └───┘
doc     └────────┘ └────────┘   └─┘          └──┘            └┘       └┘         └┘     └───┘
txt     └────────┘ └────────┘   └─┘          └──┘            └┘       └┘         └┘     └───┘
par     └────────┘ └────────┘   └─┘          └──┘            └┘       └┘         └┘     └───┘
pid               └───────┘                 └┘            └┘       └┘         └┘         
st     └──────────────────────────┘└──────┘└────┘└──────────┘└───────┘└─────────┘└──┘└──────┘
 75  theorem add_monoid.mul_smul' : ∀ (a : β) (m n : ℕ), m * n • a = n•(m•a) :=
id                                                            
src                                                                 
typ                                                           
 76  @pow_mul (multiplicative β) _
id    └─────┘  └────────────┘ 
src   └─────┘  └────────────┘
typ   └─────┘  └────────────┘ 
 77  
 78  theorem pow_mul' (a : α) (m n : ℕ) : a^(m * n) = (a^n)^m :=
id                                              
src                                                   
typ                                             
 79  by rw [mul_comm, pow_mul]
id          └──────┘  └─────┘
src     └──┘└──────┘└┘└─────┘└┘
typ     └──┘└──────┘└┘└─────┘└┘
doc     └──┘        └┘       └┘
txt     └──┘        └┘       └┘
par     └──┘        └┘       └┘
pid       └┘        └┘       
st     └───────────┘└───────┘
 80  theorem add_monoid.mul_smul (a : β) (m n : ℕ) : m * n • a = m•(n•a) :=
id                                                        
src                                                             
typ                                                       
 81  by rw [mul_comm, add_monoid.mul_smul']
id          └──────┘  └──────────────────┘
src     └──┘└──────┘└┘└──────────────────┘└─
typ     └──┘└──────┘└┘└──────────────────┘└─
doc     └──┘        └┘                    └─
txt     └──┘        └┘                    └─
par     └──┘        └┘                    └─
pid       └┘        └┘                    
st     └───────────┘└────────────────────┘
 82  
src  
typ  
doc  
txt  
par  
pid  
st   
 83  @[simp] theorem add_monoid.smul_one [has_one β] : ∀ n : ℕ, n • (1 : β) = n :=
id                                        └─────┘                       
src                                       └─────┘                         
typ                                       └─────┘                       
doc    └──┘
 84  nat.eq_cast _ (add_monoid.zero_smul _) (add_monoid.one_smul _) (add_monoid.add_smul _)
id   └─────────┘    └──────────────────┘     └─────────────────┘     └─────────────────┘
src  └─────────┘    └──────────────────┘     └─────────────────┘     └─────────────────┘
typ  └─────────┘    └──────────────────┘     └─────────────────┘     └─────────────────┘
 85  
 86  theorem pow_bit0 (a : α) (n : ℕ) : a ^ bit0 n = a^n * a^n := pow_add _ _ _
id                                      └──┘         └─────┘
src                                       └──┘              └─────┘
typ                                     └──┘         └─────┘
 87  theorem bit0_smul (a : β) (n : ℕ) : bit0 n • a = n•a + n•a := add_monoid.add_smul _ _ _
id                                     └──┘           └─────────────────┘
src                                     └──┘                 └─────────────────┘
typ                                    └──┘           └─────────────────┘
 88  
 89  theorem pow_bit1 (a : α) (n : ℕ) : a ^ bit1 n = a^n * a^n * a :=
id                                      └──┘       
src                                       └──┘           
typ                                     └──┘       
 90  by rw [bit1, pow_succ', pow_bit0]
id          └──┘  └───────┘  └──────┘
src     └──┘└──┘└┘└───────┘└┘└──────┘└┘
typ     └──┘└──┘└┘└───────┘└┘└──────┘└┘
doc     └──┘    └┘         └┘        └┘
txt     └──┘    └┘         └┘        └┘
par     └──┘    └┘         └┘        └┘
pid       └┘    └┘         └┘        
st     └───────┘└─────────┘└────────┘
 91  theorem bit1_smul : ∀ (a : β) (n : ℕ), bit1 n • a = n•a + n•a + a :=
id                                        └──┘         
src                                        └──┘              
typ                                       └──┘         
 92  @pow_bit1 (multiplicative β) _
id    └──────┘  └────────────┘ 
src   └──────┘  └────────────┘
typ   └──────┘  └────────────┘ 
 93  
 94  theorem pow_mul_comm (a : α) (m n : ℕ) : a^m * a^n = a^n * a^m :=
id                                                
src                                                       
typ                                               
 95  by rw [←pow_add, ←pow_add, add_comm]
id           └─────┘   └─────┘  └──────┘
src     └───┘└─────┘└─┘└─────┘└┘└──────┘└┘
typ     └───┘└─────┘└─┘└─────┘└┘└──────┘└┘
doc     └───┘       └─┘       └┘        └┘
txt     └───┘       └─┘       └┘        └┘
par     └───┘       └─┘       └┘        └┘
pid       └─┘       └─┘       └┘        
st     └───────────┘└────────┘└────────┘
 96  theorem smul_add_comm : ∀ (a : β) (m n : ℕ), m•a + n•a = n•a + m•a :=
id                                                    
src                                                           
typ                                                   
 97  @pow_mul_comm (multiplicative β) _
id    └──────────┘  └────────────┘ 
src   └──────────┘  └────────────┘
typ   └──────────┘  └────────────┘ 
 98  
 99  @[simp] theorem list.prod_repeat (a : α) (n : ℕ) : (list.repeat a n).prod = a ^ n :=
id                                                     └─────────┘   └──┘     
src                                                     └─────────┘     └──┘     
typ                                                    └─────────┘   └──┘     
doc    └──┘                                                              └──┘
100  by induction n with n ih; [refl, rw [list.repeat_succ, list.prod_cons, ih]]; refl
id                                      └──────────────┘  └────────────┘  └┘
src     └────────┘ └────────┘  └──┘  └──┘└──────────────┘└┘└────────────┘└┘     └───┘
typ     └────────┘└────────┘  └──┘  └──┘└──────────────┘└┘└────────────┘└┘└┘   └───┘
doc     └────────┘ └────────┘   └──┘  └──┘                └┘              └┘     └───┘
txt     └────────┘ └────────┘   └──┘  └──┘                └┘              └┘     └───┘
par     └────────┘ └────────┘   └──┘  └──┘                └┘              └┘     └───┘
pid               └───────┘           └┘                └┘              └┘         
st     └─────────────────────────────────┘└──────────────┘└──────────────┘└──┘└──────┘
101  @[simp] theorem list.sum_repeat : ∀ (a : β) (n : ℕ), (list.repeat a n).sum = n • a :=
id                                                       └─────────┘   └─┘     
src                                                       └─────────┘     └─┘     
typ                                                      └─────────┘   └─┘     
doc    └──┘                                                                └─┘
102  @list.prod_repeat (multiplicative β) _
id    └──────────────┘  └────────────┘ 
src   └──────────────┘  └────────────┘
typ   └──────────────┘  └────────────┘ 
103  
104  @[simp] lemma units.coe_pow (u : units α) (n : ℕ) : ((u ^ n : units α) : α) = u ^ n :=
id                                    └───┘                   └───┘          
src                                   └───┘                      └───┘            
typ                                   └───┘                   └───┘          
doc    └──┘
105  by induction n; simp [*, pow_succ]
id                           └──────┘
src     └────────┘   └───────┘└──────┘└─
typ     └────────┘  └───────┘└──────┘└─
doc     └────────┘   └───────┘        └─
txt     └────────┘   └───────┘        └─
par     └────────┘   └───────┘        └─
pid                     └──┘        
st     └────────────────────────────────
106  
src  
typ  
doc  
txt  
par  
pid  
st   
107  end monoid
108  
109  namespace is_monoid_hom
110  variables {β : Type v} [monoid α] [monoid β] (f : α → β) [is_monoid_hom f]
id                           └────┘     └────┘                 └───────────┘
src                          └────┘     └────┘                 └───────────┘
typ                          └────┘     └────┘                 └───────────┘
doc                                                            └───────────┘
111  
112  theorem map_pow (a : α) : ∀(n : ℕ), f (a ^ n) = (f a) ^ n
id                                                
src                                                     
typ                                               
113  | 0            := is_monoid_hom.map_one f
id                     └───────────────────┘ 
src                    └───────────────────┘
typ                    └───────────────────┘ 
114  | (nat.succ n) := by rw [pow_succ, is_monoid_hom.map_mul f, map_pow n]; refl
id      └──────┘              └──────┘  └───────────────────┘   └─────┘ 
src     └──────┘          └──┘└──────┘└┘└───────────────────┘ └┘          └────
typ     └──────┘          └──┘└──────┘└┘└───────────────────┘└┘└─────┘  └────
doc                       └──┘        └┘└───────────────────┘ └┘          └────
txt                       └──┘        └┘                      └┘          └────
par                       └──┘        └┘                      └┘          └────
pid                         └┘        └┘                      └┘              
st                       └───────────┘└───────────────────────┘└─────────┘└──────
115  
src  
typ  
doc  
txt  
par  
pid  
st   
116  end is_monoid_hom
117  
118  namespace is_add_monoid_hom
119  variables {β : Type*} [add_monoid α] [add_monoid β] (f : α → β) [is_add_monoid_hom f]
id                          └────────┘     └────────┘                 └───────────────┘
src                         └────────┘     └────────┘                 └───────────────┘
typ                         └────────┘     └────────┘                 └───────────────┘
doc                                                                   └───────────────┘
120  
121  theorem map_smul (a : α) : ∀(n : ℕ), f (n • a) = n • (f a)
id                                                
src                                                  
typ                                               
122  | 0            := is_add_monoid_hom.map_zero f
id                     └────────────────────────┘ 
src                    └────────────────────────┘
typ                    └────────────────────────┘ 
123  | (nat.succ n) := by rw [succ_smul, is_add_monoid_hom.map_add f, map_smul n]; refl
id      └──────┘              └───────┘  └───────────────────────┘   └──────┘ 
src     └──────┘          └──┘└───────┘└┘└───────────────────────┘ └┘           └────
typ     └──────┘          └──┘└───────┘└┘└───────────────────────┘└┘└──────┘  └────
doc                       └──┘         └┘                          └┘           └────
txt                       └──┘         └┘                          └┘           └────
par                       └──┘         └┘                          └┘           └────
pid                         └┘         └┘                          └┘               
st                       └────────────┘└───────────────────────────┘└──────────┘└──────
124  
src  
typ  
doc  
txt  
par  
pid  
st   
125  end is_add_monoid_hom
126  
127  namespace monoid_hom
128  variables {β : Type v} [monoid α] [monoid β] (f : α →* β)
id                           └────┘     └────┘           └┘
src                          └────┘     └────┘           └┘
typ                          └────┘     └────┘           └┘
doc                                                      └┘
129  
130  @[simp] theorem map_pow (a : α) : ∀(n : ℕ), f (a ^ n) = (f a) ^ n
id                                                        
src                                                             
typ                                                       
doc    └──┘
131  | 0            := f.map_one
id                     └──────┘
src                     └──────┘
typ                    └──────┘
doc                     └──────┘
132  | (nat.succ n) := by rw [pow_succ, f.map_mul, map_pow n]; refl
id      └──────┘              └──────┘             └─────┘ 
src     └──────┘          └──┘└──────┘└┘         └┘          └────
typ     └──────┘          └──┘└──────┘└┘└───────┘└┘└─────┘  └────
doc                       └──┘        └┘         └┘          └────
txt                       └──┘        └┘         └┘          └────
par                       └──┘        └┘         └┘          └────
pid                         └┘        └┘         └┘              
st                       └───────────┘└─────────┘└─────────┘└──────
133  
src  
typ  
doc  
txt  
par  
pid  
st   
134  end monoid_hom
135  
136  namespace add_monoid_hom
137  variables {β : Type*} [add_monoid α] [add_monoid β] (f : α →+ β)
id                          └────────┘     └────────┘           └┘
src                         └────────┘     └────────┘           └┘
typ                         └────────┘     └────────┘           └┘
doc                                                             └┘
138  
139  @[simp] theorem map_smul (a : α) : ∀(n : ℕ), f (n • a) = n • (f a)
id                                                        
src                                                          
typ                                                       
doc    └──┘
140  | 0            := f.map_zero
id                     └───────┘
src                     └───────┘
typ                    └───────┘
141  | (nat.succ n) := by rw [succ_smul, f.map_add, map_smul n]; refl
id      └──────┘              └───────┘             └──────┘ 
src     └──────┘          └──┘└───────┘└┘         └┘           └────
typ     └──────┘          └──┘└───────┘└┘└───────┘└┘└──────┘  └────
doc                       └──┘         └┘         └┘           └────
txt                       └──┘         └┘         └┘           └────
par                       └──┘         └┘         └┘           └────
pid                         └┘         └┘         └┘               
st                       └────────────┘└─────────┘└──────────┘└──────
142  
src  
typ  
doc  
txt  
par  
pid  
st   
143  end add_monoid_hom
144  
145  @[simp] theorem nat.pow_eq_pow (p q : ℕ) :
id                                         
src                                        
typ                                        
doc    └──┘
146    @has_pow.pow _ _ monoid.has_pow p q = p ^ q :=
id      └─────────┘     └────────────┘      
src     └─────────┘     └────────────┘        
typ     └─────────┘     └────────────┘      
147  by induction q with q ih; [refl, rw [nat.pow_succ, pow_succ, mul_comm, ih]]
id                                      └──────────┘  └──────┘  └──────┘  └┘
src     └────────┘ └────────┘  └──┘  └──┘└──────────┘└┘└──────┘└┘└──────┘└┘  
typ     └────────┘└────────┘  └──┘  └──┘└──────────┘└┘└──────┘└┘└──────┘└┘└┘
doc     └────────┘ └────────┘   └──┘  └──┘            └┘        └┘        └┘  
txt     └────────┘ └────────┘   └──┘  └──┘            └┘        └┘        └┘  
par     └────────┘ └────────┘   └──┘  └──┘            └┘        └┘        └┘  
pid               └───────┘           └┘            └┘        └┘        └┘  
st     └─────────────────────────────────┘└──────────┘└────────┘└────────┘└──┘
148  
149  @[simp] theorem nat.smul_eq_mul (m n : ℕ) : m • n = m * n :=
id                                                    
src                                                     
typ                                                   
doc    └──┘
150  by induction m with m ih; [rw [add_monoid.zero_smul, zero_mul],
id                                └──────────────────┘  └──────┘
src     └────────┘ └────────┘  └──┘└──────────────────┘└┘└──────┘
typ     └────────┘└────────┘  └──┘└──────────────────┘└┘└──────┘
doc     └────────┘ └────────┘   └──┘                    └┘        
txt     └────────┘ └────────┘   └──┘                    └┘        
par     └────────┘ └────────┘   └──┘                    └┘        
pid               └───────┘     └┘                    └┘        
st     └───────────────────────────┘└──────────────────┘└────────┘└─
151    rw [succ_smul', ih, nat.succ_mul]]
id         └────────┘  └┘  └──────────┘
src    └──┘└────────┘└┘  └┘└──────────┘
typ    └──┘└────────┘└┘└┘└┘└──────────┘
doc    └──┘          └┘  └┘            
txt    └──┘          └┘  └┘            
par    └──┘          └┘  └┘            
pid      └┘          └┘  └┘            
st   ─────┘└────────┘└──┘└────────────┘
152  
153  /- commutative monoid -/
154  
155  section comm_monoid
156  variables [comm_monoid α] {β : Type*} [add_comm_monoid β]
id              └─────────┘                 └─────────────┘
src             └─────────┘                 └─────────────┘
typ             └─────────┘                 └─────────────┘
157  
158  theorem mul_pow (a b : α) (n : ℕ) : (a * b)^n = a^n * b^n :=
id                                             
src                                                   
typ                                            
159  by induction n with n ih; [exact (mul_one _).symm,
id                                   └─────┘
src     └────────┘ └────────┘  └────┘ └─────┘└──────┘
typ     └────────┘└────────┘  └────┘ └─────┘└──────┘
doc     └────────┘ └────────┘   └────┘        └──────┘
txt     └────────┘ └────────┘   └────┘        └──────┘
par     └────────┘ └────────┘   └────┘        └──────┘
pid               └───────┘                └─────┘
st     └────────────────────────────────────────────────
160    simp only [pow_succ, ih, mul_assoc, mul_left_comm]]
id                └──────┘  └┘  └───────┘  └───────────┘
src    └─────────┘└──────┘└┘  └┘└───────┘└┘└───────────┘
typ    └─────────┘└──────┘└┘└┘└┘└───────┘└┘└───────────┘
doc    └─────────┘        └┘  └┘         └┘             
txt    └─────────┘        └┘  └┘         └┘             
par    └─────────┘        └┘  └┘         └┘             
pid        └──┘└┘        └┘  └┘         └┘             
st   ────────────────────────────────────────────────────┘
161  theorem add_monoid.smul_add : ∀ (a b : β) (n : ℕ), n•(a + b) = n•a + n•b :=
id                                                            
src                                                                  
typ                                                           
162  @mul_pow (multiplicative β) _
id    └─────┘  └────────────┘ 
src   └─────┘  └────────────┘
typ   └─────┘  └────────────┘ 
163  
164  instance pow.is_monoid_hom (n : ℕ) : is_monoid_hom ((^ n) : α → α) :=
id                                       └───────────┘           
src                                      └───────────┘  
typ                                      └───────────┘           
doc                                       └───────────┘
165  { map_mul := λ _ _, mul_pow _ _ _, map_one := one_pow _ }
id                     └─────┘                   └─────┘
src                      └─────┘                   └─────┘
typ                    └─────┘                   └─────┘
166  
167  instance add_monoid.smul.is_add_monoid_hom (n : ℕ) : is_add_monoid_hom (add_monoid.smul n : β → β) :=
id                                                       └───────────────┘  └─────────────┘       
src                                                      └───────────────┘  └─────────────┘
typ                                                      └───────────────┘  └─────────────┘       
doc                                                       └───────────────┘
168  { map_add := λ _ _, add_monoid.smul_add _ _ _, map_zero := add_monoid.smul_zero _ }
id                     └─────────────────┘                    └──────────────────┘
src                      └─────────────────┘                    └──────────────────┘
typ                    └─────────────────┘                    └──────────────────┘
169  
170  end comm_monoid
171  
172  section group
173  variables [group α] {β : Type*} [add_group β]
id              └───┘                 └───────┘
src             └───┘                 └───────┘
typ             └───┘                 └───────┘
174  
175  section nat
176  
177  @[simp] theorem inv_pow (a : α) (n : ℕ) : (a⁻¹)^n = (a^n)⁻¹ :=
id                                            └┘     └┘
src                                             └┘        └┘
typ                                           └┘     └┘
doc    └──┘
178  by induction n with n ih; [exact one_inv.symm,
id                                  └──────────┘
src     └────────┘ └────────┘  └────┘└──────────┘
typ     └────────┘└────────┘  └────┘└──────────┘
doc     └────────┘ └────────┘   └────┘
txt     └────────┘ └────────┘   └────┘
par     └────────┘ └────────┘   └────┘
pid               └───────┘        
st     └────────────────────────────────────────────
179    rw [pow_succ', pow_succ, ih, mul_inv_rev]]
id         └───────┘  └──────┘  └┘  └─────────┘
src    └──┘└───────┘└┘└──────┘└┘  └┘└─────────┘
typ    └──┘└───────┘└┘└──────┘└┘└┘└┘└─────────┘
doc    └──┘         └┘        └┘  └┘           
txt    └──┘         └┘        └┘  └┘           
par    └──┘         └┘        └┘  └┘           
pid      └┘         └┘        └┘  └┘           
st   ─────┘└───────┘└────────┘└──┘└───────────┘
180  @[simp] theorem add_monoid.neg_smul : ∀ (a : β) (n : ℕ), n•(-a) = -(n•a) :=
id                                                               
src                                                                  
typ                                                              
doc    └──┘
181  @inv_pow (multiplicative β) _
id    └─────┘  └────────────┘ 
src   └─────┘  └────────────┘
typ   └─────┘  └────────────┘ 
182  
183  theorem pow_sub (a : α) {m n : ℕ} (h : n ≤ m) : a^(m - n) = a^m * (a^n)⁻¹ :=
id                                                        └┘
src                                                                 └┘
typ                                                       └┘
184  have h1 : m - n + n = m, from nat.sub_add_cancel h,
id                          └────────────────┘ 
src                             └────────────────┘
typ                         └────────────────┘ 
185  have h2 : a^(m - n) * a^n = a^m, by rw [←pow_add, h1],
id                               └─────┘  └┘
src                                └───┘└─────┘└┘  
typ                         └───┘└─────┘└┘└┘
doc                                      └───┘       └┘  
txt                                      └───┘       └┘  
par                                      └───┘       └┘  
pid                                        └─┘       └┘  
st                                      └───────────┘└──┘
186  eq_mul_inv_of_mul_eq h2
id   └──────────────────┘ └┘
src  └──────────────────┘
typ  └──────────────────┘ └┘
187  theorem add_monoid.smul_sub : ∀ (a : β) {m n : ℕ}, n ≤ m → (m - n)•a = m•a - n•a :=
id                                                                 
src                                                                         
typ                                                                
188  @pow_sub (multiplicative β) _
id    └─────┘  └────────────┘ 
src   └─────┘  └────────────┘
typ   └─────┘  └────────────┘ 
189  
190  theorem pow_inv_comm (a : α) (m n : ℕ) : (a⁻¹)^m * a^n = a^n * (a⁻¹)^m :=
id                                           └┘        └┘ 
src                                            └┘              └┘ 
typ                                          └┘        └┘ 
191  by rw inv_pow; exact inv_comm_of_comm (pow_mul_comm _ _ _)
id         └─────┘        └──────────────┘  └──────────┘
src     └─┘└─────┘  └────┘└──────────────┘ └──────────┘└──────┘
typ     └─┘└─────┘  └────┘└──────────────┘ └──────────┘└──────┘
doc     └─┘         └────┘                             └──────┘
txt     └─┘         └────┘                             └──────┘
par     └─┘         └────┘                             └──────┘
pid                                                  └─────┘
st     └───────────────────────────────────────────────────────┘
192  theorem add_monoid.smul_neg_comm : ∀ (a : β) (m n : ℕ), m•(-a) + n•a = n•a + m•(-a) :=
id                                                                  
src                                                                         
typ                                                                 
193  @pow_inv_comm (multiplicative β) _
id    └──────────┘  └────────────┘ 
src   └──────────┘  └────────────┘
typ   └──────────┘  └────────────┘ 
194  end nat
195  
196  open int
197  
198  /--
199  The power operation in a group. This extends `monoid.pow` to negative integers
200  with the definition `a^(-n) = (a^n)⁻¹`.
201  -/
202  def gpow (a : α) : ℤ → α
id                       
src                     
typ                      
203  | (of_nat n) := a^n
id      └────┘      
src     └────┘        
typ     └────┘      
204  | -[1+n]     := (a^(nat.succ n))⁻¹
id     └──┘          └──────┘    └┘
src    └──┘            └──────┘    └┘
typ    └──┘          └──────┘    └┘
205  
206  def gsmul (n : ℤ) (a : β) : β :=
id                             
src                 
typ                            
207  @gpow (multiplicative β) _ a n
id    └──┘  └────────────┘      
src   └──┘  └────────────┘
typ   └──┘  └────────────┘      
doc   └──┘
208  
209  @[priority 10] instance group.has_pow : has_pow α ℤ := ⟨gpow⟩
id                                           └─────┘       └──┘
src                                          └─────┘        └──┘
typ                                          └─────┘       └──┘
doc                                                          └──┘
210  
211  localized "infix ` • `:70 := gsmul" in add_group
212  localized "infix ` •ℕ `:70 := add_monoid.smul" in smul
213  localized "infix ` •ℤ `:70 := gsmul" in smul
214  
215  @[simp] theorem gpow_coe_nat (a : α) (n : ℕ) : a ^ (n:ℤ) = a ^ n := rfl
id                                                             └─┘
src                                                                 └─┘
typ                                                            └─┘
doc    └──┘
216  @[simp] theorem gsmul_coe_nat (a : β) (n : ℕ) : (n:ℤ) • a = n •ℕ a := rfl
id                                                         └┘     └─┘
src                                                            └┘      └─┘
typ                                                        └┘     └─┘
doc    └──┘
217  
218  @[simp] theorem gpow_of_nat (a : α) (n : ℕ) : a ^ of_nat n = a ^ n := rfl
id                                                 └────┘         └─┘
src                                                  └────┘            └─┘
typ                                                └────┘         └─┘
doc    └──┘
219  @[simp] theorem gsmul_of_nat (a : β) (n : ℕ) : of_nat n • a = n •ℕ a := rfl
id                                                └────┘      └┘     └─┘
src                                                └────┘         └┘      └─┘
typ                                               └────┘      └┘     └─┘
doc    └──┘
220  
221  @[simp] theorem gpow_neg_succ (a : α) (n : ℕ) : a ^ -[1+n] = (a ^ n.succ)⁻¹ := rfl
id                                                   └──┘     └───┘ └┘    └─┘
src                                                    └──┘        └───┘ └┘    └─┘
typ                                                  └──┘     └───┘ └┘    └─┘
doc    └──┘
222  @[simp] theorem gsmul_neg_succ (a : β) (n : ℕ) : -[1+n] • a = - (n.succ •ℕ a) := rfl
id                                                  └──┘      └───┘ └┘      └─┘
src                                                  └──┘         └───┘ └┘       └─┘
typ                                                 └──┘      └───┘ └┘      └─┘
doc    └──┘
223  
224  local attribute [ematch] le_of_lt
id                            └──────┘
src                   └────┘  └──────┘
typ                           └──────┘
doc                   └────┘
225  open nat
226  
227  @[simp] theorem gpow_zero (a : α) : a ^ (0:ℤ) = 1 := rfl
id                                                   └─┘
src                                                    └─┘
typ                                                  └─┘
doc    └──┘
228  @[simp] theorem zero_gsmul (a : β) : (0:ℤ) • a = 0 := rfl
id                                                    └─┘
src                                                     └─┘
typ                                                   └─┘
doc    └──┘
229  
230  @[simp] theorem gpow_one (a : α) : a ^ (1:ℤ) = a := mul_one _
id                                                 └─────┘
src                                                   └─────┘
typ                                                └─────┘
doc    └──┘
231  @[simp] theorem one_gsmul (a : β) : (1:ℤ) • a = a := add_zero _
id                                                  └──────┘
src                                                    └──────┘
typ                                                 └──────┘
doc    └──┘
232  
233  @[simp] theorem one_gpow : ∀ (n : ℤ), (1 : α) ^ n = 1
id                                                
src                                                  
typ                                               
doc    └──┘
234  | (n : ℕ) := one_pow _
id               └─────┘
src              └─────┘
typ              └─────┘
235  | -[1+ n] := show _⁻¹=(1:α), by rw [_root_.one_pow, one_inv]
id     └──┘            └┘             └────────────┘  └─────┘
src    └──┘            └┘          └──┘└────────────┘└┘└─────┘└┘
typ    └──┘            └┘         └──┘└────────────┘└┘└─────┘└┘
doc                                  └──┘              └┘       └┘
txt                                  └──┘              └┘       └┘
par                                  └──┘              └┘       └┘
pid                                    └┘              └┘       
st                                  └─────────────────┘└───────┘
236  @[simp] theorem gsmul_zero : ∀ (n : ℤ), n • (0 : β) = 0 :=
id                                                   
src                                                    
typ                                                  
doc    └──┘
237  @one_gpow (multiplicative β) _
id    └──────┘  └────────────┘ 
src   └──────┘  └────────────┘
typ   └──────┘  └────────────┘ 
238  
239  @[simp] theorem gpow_neg (a : α) : ∀ (n : ℤ), a ^ -n = (a ^ n)⁻¹
id                                                      └┘
src                                                           └┘
typ                                                     └┘
doc    └──┘
240  | (n+1:ℕ) := rfl
id              └─┘
src             └─┘
typ             └─┘
241  | 0       := one_inv.symm
id                └─────┘└───┘
src               └─────┘└───┘
typ               └─────┘└───┘
242  | -[1+ n] := (inv_inv _).symm
id     └──┘       └─────┘   └──┘
src    └──┘       └─────┘   └──┘
typ    └──┘       └─────┘   └──┘
243  
244  @[simp] theorem neg_gsmul : ∀ (a : β) (n : ℤ), -n • a = -(n • a) :=
id                                                       
src                                                         
typ                                                      
doc    └──┘
245  @gpow_neg (multiplicative β) _
id    └──────┘  └────────────┘ 
src   └──────┘  └────────────┘
typ   └──────┘  └────────────┘ 
246  
247  theorem gpow_neg_one (x : α) : x ^ (-1:ℤ) = x⁻¹ := congr_arg has_inv.inv $ pow_one x
id                                         └┘    └───────┘ └─────────┘   └─────┘ 
src                                           └┘    └───────┘ └─────────┘   └─────┘
typ                                        └┘    └───────┘ └─────────┘   └─────┘ 
248  theorem neg_one_gsmul (x : β) : (-1:ℤ) • x = -x := congr_arg has_neg.neg $ add_monoid.one_smul x
id                                              └───────┘ └─────────┘   └─────────────────┘ 
src                                                └───────┘ └─────────┘   └─────────────────┘
typ                                             └───────┘ └─────────┘   └─────────────────┘ 
249  
250  theorem gsmul_one [has_one β] (n : ℤ) : n • (1 : β) = n :=
id                      └─────┘                      
src                     └─────┘                        
typ                     └─────┘                      
251  begin
st   └─────
252  cases n,
id         
src  └────┘
typ  └────┘
doc  └────┘
txt  └────┘
par  └────┘
pid       
st   ──────┘└─
253    { rw [gsmul_of_nat, add_monoid.smul_one, int.cast_of_nat] },
id           └──────────┘  └─────────────────┘  └─────────────┘
src      └──┘└──────────┘└┘└─────────────────┘└┘└─────────────┘└┘
typ      └──┘└──────────┘└┘└─────────────────┘└┘└─────────────┘└┘
doc      └──┘            └┘                   └┘               └┘
txt      └──┘            └┘                   └┘               └┘
par      └──┘            └┘                   └┘               └┘
pid        └┘            └┘                   └┘               
st   ───┘└──────────────┘└───────────────────┘└───────────────┘└┘
254    { rw [gsmul_neg_succ, add_monoid.smul_one, int.cast_neg_succ_of_nat, nat.cast_succ] }
id           └────────────┘  └─────────────────┘  └──────────────────────┘  └───────────┘
src      └──┘└────────────┘└┘└─────────────────┘└┘└──────────────────────┘└┘└───────────┘└┘
typ      └──┘└────────────┘└┘└─────────────────┘└┘└──────────────────────┘└┘└───────────┘└┘
doc      └──┘              └┘                   └┘                        └┘             └┘
txt      └──┘              └┘                   └┘                        └┘             └┘
par      └──┘              └┘                   └┘                        └┘             └┘
pid        └┘              └┘                   └┘                        └┘             
st   ─────────────────────┘└───────────────────┘└────────────────────────┘└─────────────┘└─
255  end
st   ──┘
256  
257  theorem inv_gpow (a : α) : ∀n:ℤ, a⁻¹ ^ n = (a ^ n)⁻¹
id                                 └┘        └┘
src                                   └┘           └┘
typ                                └┘        └┘
258  | (n : ℕ) := inv_pow a n
id              └─────┘ 
src              └─────┘
typ             └─────┘ 
259  | -[1+ n] := congr_arg has_inv.inv $ inv_pow a (n+1)
id     └──┘     └───────┘ └─────────┘   └─────┘    
src    └──┘      └───────┘ └─────────┘   └─────┘     
typ    └──┘     └───────┘ └─────────┘   └─────┘    
260  
261  private lemma gpow_add_aux (a : α) (m n : nat) :
id                                            └─┘
src                                            └─┘
typ                                           └─┘
262    a ^ ((of_nat m) + -[1+n]) = a ^ of_nat m * a ^ -[1+n] :=
id         └────┘    └──┘     └────┘     └──┘
src         └────┘     └──┘       └────┘       └──┘ 
typ        └────┘    └──┘     └────┘     └──┘
263  or.elim (nat.lt_or_ge m (nat.succ n))
id   └─────┘  └──────────┘   └──────┘ 
src  └─────┘  └──────────┘    └──────┘
typ  └─────┘  └──────────┘   └──────┘ 
264   (assume h1 : m < succ n,
id                   └──┘ 
src                   └──┘
typ                  └──┘ 
265    have h2 : m ≤ n, from le_of_lt_succ h1,
id                        └───────────┘ └┘
src                         └───────────┘
typ                       └───────────┘ └┘
266    suffices a ^ -[1+ n-m] = a ^ of_nat m * a ^ -[1+n],
id                └──┘     └────┘     └──┘
src                └──┘        └────┘       └──┘ 
typ               └──┘     └────┘     └──┘
267      by rwa [of_nat_add_neg_succ_of_nat_of_lt h1],
id               └──────────────────────────────┘ └┘
src         └───┘└──────────────────────────────┘  
typ         └───┘└──────────────────────────────┘└┘
doc         └───┘                                  
txt         └───┘                                  
par         └───┘                                  
pid            └┘                                  
st         └───────────────────────────────────────┘
268    show (a ^ nat.succ (n - m))⁻¹ = a ^ of_nat m * a ^ -[1+n],
id             └──────┘      └┘    └────┘     └──┘
src             └──────┘        └┘     └────┘       └──┘ 
typ            └──────┘      └┘    └────┘     └──┘
269    by rw [← succ_sub h2, pow_sub _ (le_of_lt h1), mul_inv_rev, inv_inv]; refl)
id              └──────┘ └┘  └─────┘    └──────┘ └┘   └─────────┘  └─────┘
src       └────┘└──────┘  └┘└─────┘└─┘ └──────┘  └─┘└─────────┘└┘└─────┘  └──┘
typ       └────┘└──────┘└┘└┘└─────┘└─┘ └──────┘└┘└─┘└─────────┘└┘└─────┘  └──┘
doc       └────┘          └┘       └─┘           └─┘           └┘         └──┘
txt       └────┘          └┘       └─┘           └─┘           └┘         └──┘
par       └────┘          └┘       └─┘           └─┘           └┘         └──┘
pid         └──┘          └┘       └─┘           └─┘           └┘       
st       └────────────────┘└───────────────────────┘└───────────┘└───────┘└────┘
270   (assume : m ≥ succ n,
id                └──┘ 
src                └──┘
typ               └──┘ 
271    suffices a ^ (of_nat (m - succ n)) = (a ^ (of_nat m)) * (a ^ -[1+ n]),
id                 └────┘    └──┘         └────┘        └──┘ 
src                 └────┘     └──┘           └────┘          └──┘  
typ                └────┘    └──┘         └────┘        └──┘ 
272      by rw [of_nat_add_neg_succ_of_nat_of_ge]; assumption,
id              └──────────────────────────────┘
src         └──┘└──────────────────────────────┘  └────────┘
typ         └──┘└──────────────────────────────┘  └────────┘
doc         └──┘                                  └────────┘
txt         └──┘                                  └────────┘
par         └──┘                                  └────────┘
pid           └┘                                
st         └───────────────────────────────────┘└──────────┘
273    suffices a ^ (m - succ n) = a ^ m * (a ^ n.succ)⁻¹, from this,
id                   └──┘           └───┘ └┘       └──┘
src                    └──┘                └───┘ └┘
typ                  └──┘           └───┘ └┘       └──┘
274    by rw pow_sub; assumption)
id           └─────┘
src       └─┘└─────┘  └────────┘
typ       └─┘└─────┘  └────────┘
doc       └─┘         └────────┘
txt       └─┘         └────────┘
par       └─┘         └────────┘
pid         
st       └─────────────────────┘
275  
276  theorem gpow_add (a : α) : ∀ (i j : ℤ), a ^ (i + j) = a ^ i * a ^ j
id                                                      
src                                                            
typ                                                     
277  | (of_nat m) (of_nat n) := pow_add _ _ _
id                 └────┘       └─────┘
src                └────┘       └─────┘
typ                └────┘       └─────┘
278  | (of_nat m) -[1+n]     := gpow_add_aux _ _ _
id      └────┘    └──┘         └──────────┘
src     └────┘    └──┘         └──────────┘
typ     └────┘    └──┘         └──────────┘
279  | -[1+m]     (of_nat n) := by rw [add_comm, gpow_add_aux,
id     └──┘       └────┘              └──────┘  └──────────┘
src    └──┘       └────┘          └──┘└──────┘└┘└──────────┘└─
typ    └──┘       └────┘          └──┘└──────┘└┘└──────────┘└─
doc                                └──┘        └┘            └─
txt                                └──┘        └┘            └─
par                                └──┘        └┘            └─
pid                                  └┘        └┘            └─
st                                └───────────┘└────────────┘└─
280    gpow_neg_succ, gpow_of_nat, ← inv_pow, ← pow_inv_comm]
id     └───────────┘  └─────────┘    └─────┘    └──────────┘
src  ─┘└───────────┘└┘└─────────┘└──┘└─────┘└──┘└──────────┘└┘
typ  ─┘└───────────┘└┘└─────────┘└──┘└─────┘└──┘└──────────┘└┘
doc  ─┘             └┘           └──┘       └──┘            └┘
txt  ─┘             └┘           └──┘       └──┘            └┘
par  ─┘             └┘           └──┘       └──┘            └┘
pid  ─┘             └┘           └──┘       └──┘            
st   ──────────────┘└───────────┘└─────────┘└──────────────┘
281  | -[1+m]     -[1+n]     :=
id     └──┘     └──┘
src    └──┘      └──┘ 
typ    └──┘     └──┘
282    suffices (a ^ (m + succ (succ n)))⁻¹ = (a ^ m.succ)⁻¹ * (a ^ n.succ)⁻¹, from this,
id                     └──┘  └──┘     └┘      └───┘ └┘      └───┘ └┘       └──┘
src                     └──┘  └──┘     └┘       └───┘ └┘       └───┘ └┘
typ                    └──┘  └──┘     └┘      └───┘ └┘      └───┘ └┘       └──┘
283    by rw [← succ_add_eq_succ_add, add_comm, _root_.pow_add, mul_inv_rev]
id              └──────────────────┘  └──────┘  └────────────┘  └─────────┘
src       └────┘└──────────────────┘└┘└──────┘└┘└────────────┘└┘└─────────┘└─
typ       └────┘└──────────────────┘└┘└──────┘└┘└────────────┘└┘└─────────┘└─
doc       └────┘                    └┘        └┘              └┘           └─
txt       └────┘                    └┘        └┘              └┘           └─
par       └────┘                    └┘        └┘              └┘           └─
pid         └──┘                    └┘        └┘              └┘           
st       └─────────────────────────┘└────────┘└──────────────┘└───────────┘
284  
src  
typ  
doc  
txt  
par  
pid  
st   
285  theorem add_gsmul : ∀ (a : β) (i j : ℤ), (i + j) • a = i • a + j • a :=
id                                                        
src                                                             
typ                                                       
286  @gpow_add (multiplicative β) _
id    └──────┘  └────────────┘ 
src   └──────┘  └────────────┘
typ   └──────┘  └────────────┘ 
287  
288  theorem gpow_add_one (a : α) (i : ℤ) : a ^ (i + 1) = a ^ i * a :=
id                                                     
src                                                        
typ                                                    
289  by rw [gpow_add, gpow_one]
id          └──────┘  └──────┘
src     └──┘└──────┘└┘└──────┘└┘
typ     └──┘└──────┘└┘└──────┘└┘
doc     └──┘        └┘        └┘
txt     └──┘        └┘        └┘
par     └──┘        └┘        └┘
pid       └┘        └┘        
st     └───────────┘└────────┘
290  theorem add_one_gsmul : ∀ (a : β) (i : ℤ), (i + 1) • a = i • a + a :=
id                                                         
src                                                            
typ                                                        
291  @gpow_add_one (multiplicative β) _
id    └──────────┘  └────────────┘ 
src   └──────────┘  └────────────┘
typ   └──────────┘  └────────────┘ 
292  
293  theorem gpow_one_add (a : α) (i : ℤ) : a ^ (1 + i) = a * a ^ i :=
id                                                     
src                                                        
typ                                                    
294  by rw [gpow_add, gpow_one]
id          └──────┘  └──────┘
src     └──┘└──────┘└┘└──────┘└┘
typ     └──┘└──────┘└┘└──────┘└┘
doc     └──┘        └┘        └┘
txt     └──┘        └┘        └┘
par     └──┘        └┘        └┘
pid       └┘        └┘        
st     └───────────┘└────────┘
295  theorem one_add_gsmul : ∀ (a : β) (i : ℤ), (1 + i) • a = a + i • a :=
id                                                         
src                                                            
typ                                                        
296  @gpow_one_add (multiplicative β) _
id    └──────────┘  └────────────┘ 
src   └──────────┘  └────────────┘
typ   └──────────┘  └────────────┘ 
297  
298  theorem gpow_mul_comm (a : α) (i j : ℤ) : a ^ i * a ^ j = a ^ j * a ^ i :=
id                                                         
src                                                               
typ                                                        
299  by rw [← gpow_add, ← gpow_add, add_comm]
id            └──────┘    └──────┘  └──────┘
src     └────┘└──────┘└──┘└──────┘└┘└──────┘└┘
typ     └────┘└──────┘└──┘└──────┘└┘└──────┘└┘
doc     └────┘        └──┘        └┘        └┘
txt     └────┘        └──┘        └┘        └┘
par     └────┘        └──┘        └┘        └┘
pid       └──┘        └──┘        └┘        
st     └─────────────┘└──────────┘└────────┘
300  theorem gsmul_add_comm : ∀ (a : β) (i j), i • a + j • a = j • a + i • a :=
id                                                        
src                                                                
typ                                                       
301  @gpow_mul_comm (multiplicative β) _
id    └───────────┘  └────────────┘ 
src   └───────────┘  └────────────┘
typ   └───────────┘  └────────────┘ 
302  
303  theorem gpow_mul (a : α) : ∀ m n : ℤ, a ^ (m * n) = (a ^ m) ^ n
id                                                    
src                                                         
typ                                                   
304  | (m : ℕ) (n : ℕ) := pow_mul _ _ _
id                      └─────┘
src                     └─────┘
typ                     └─────┘
305  | (m : ℕ) -[1+ n] := (gpow_neg _ (m * succ n)).trans $
id           └──┘      └──────┘       └──┘    └───┘
src           └──┘       └──────┘       └──┘    └───┘
typ          └──┘      └──────┘       └──┘    └───┘
doc                                        └──┘
306    show (a ^ (m * succ n))⁻¹ = _, by rw pow_mul; refl
id                 └──┘    └┘           └─────┘
src                 └──┘    └┘        └─┘└─────┘  └───┘
typ                └──┘    └┘        └─┘└─────┘  └───┘
doc                                      └─┘         └───┘
txt                                      └─┘         └───┘
par                                      └─┘         └───┘
pid                                                     
st                                      └────────────────┘
307  | -[1+ m] (n : ℕ) := (gpow_neg _ (succ m * n)).trans $
id     └──┘            └──────┘    └──┘       └───┘
src    └──┘              └──────┘    └──┘       └───┘
typ    └──┘            └──────┘    └──┘       └───┘
doc                                    └──┘
308    show (a ^ (m.succ * n))⁻¹ = _, by rw [pow_mul, ← inv_pow]; refl
id               └───┘     └┘            └─────┘    └─────┘
src               └───┘     └┘        └──┘└─────┘└──┘└─────┘  └───┘
typ              └───┘     └┘        └──┘└─────┘└──┘└─────┘  └───┘
doc                                      └──┘       └──┘         └───┘
txt                                      └──┘       └──┘         └───┘
par                                      └──┘       └──┘         └───┘
pid                                        └┘       └──┘             
st                                      └──────────┘└─────────┘└─────┘
309  | -[1+ m] -[1+ n] := (pow_mul a (succ m) (succ n)).trans $
id     └──┘  └──┘      └─────┘   └──┘     └──┘    └───┘
src    └──┘   └──┘       └─────┘    └──┘     └──┘    └───┘
typ    └──┘  └──┘      └─────┘   └──┘     └──┘    └───┘
310    show _ = (_⁻¹^_)⁻¹, by rw [inv_pow, inv_inv]
id               └┘  └┘         └─────┘  └─────┘
src              └┘  └┘     └──┘└─────┘└┘└─────┘└┘
typ              └┘  └┘     └──┘└─────┘└┘└─────┘└┘
doc                           └──┘       └┘       └┘
txt                           └──┘       └┘       └┘
par                           └──┘       └┘       └┘
pid                             └┘       └┘       
st                           └──────────┘└───────┘
311  theorem gsmul_mul' : ∀ (a : β) (m n : ℤ), m * n • a = n • (m • a) :=
id                                                      
src                                                          
typ                                                     
312  @gpow_mul (multiplicative β) _
id    └──────┘  └────────────┘ 
src   └──────┘  └────────────┘
typ   └──────┘  └────────────┘ 
313  
314  theorem gpow_mul' (a : α) (m n : ℤ) : a ^ (m * n) = (a ^ n) ^ m :=
id                                                     
src                                                         
typ                                                    
315  by rw [mul_comm, gpow_mul]
id          └──────┘  └──────┘
src     └──┘└──────┘└┘└──────┘└┘
typ     └──┘└──────┘└┘└──────┘└┘
doc     └──┘        └┘        └┘
txt     └──┘        └┘        └┘
par     └──┘        └┘        └┘
pid       └┘        └┘        
st     └───────────┘└────────┘
316  theorem gsmul_mul (a : β) (m n : ℤ) : m * n • a = m • (n • a) :=
id                                                  
src                                                      
typ                                                 
317  by rw [mul_comm, gsmul_mul']
id          └──────┘  └────────┘
src     └──┘└──────┘└┘└────────┘└─
typ     └──┘└──────┘└┘└────────┘└─
doc     └──┘        └┘          └─
txt     └──┘        └┘          └─
par     └──┘        └┘          └─
pid       └┘        └┘          
st     └───────────┘└──────────┘
318  
src  
typ  
doc  
txt  
par  
pid  
st   
319  theorem gpow_bit0 (a : α) (n : ℤ) : a ^ bit0 n = a ^ n * a ^ n := gpow_add _ _ _
id                                       └──┘             └──────┘
src                                        └──┘                  └──────┘
typ                                      └──┘             └──────┘
320  theorem bit0_gsmul (a : β) (n : ℤ) : bit0 n • a = n • a + n • a := gpow_add _ _ _
id                                      └──┘               └──────┘
src                                      └──┘                     └──────┘
typ                                     └──┘               └──────┘
321  
322  theorem gpow_bit1 (a : α) (n : ℤ) : a ^ bit1 n = a ^ n * a ^ n * a :=
id                                       └──┘           
src                                        └──┘               
typ                                      └──┘           
323  by rw [bit1, gpow_add]; simp [gpow_bit0]
id          └──┘  └──────┘         └───────┘
src     └──┘└──┘└┘└──────┘  └────┘└───────┘└┘
typ     └──┘└──┘└┘└──────┘  └────┘└───────┘└┘
doc     └──┘    └┘          └────┘         └┘
txt     └──┘    └┘          └────┘         └┘
par     └──┘    └┘          └────┘         └┘
pid       └┘    └┘                       
st     └───────┘└────────┘└─────────────────┘
324  theorem bit1_gsmul : ∀ (a : β) (n : ℤ), bit1 n • a = n • a + n • a + a :=
id                                         └──┘             
src                                         └──┘                  
typ                                        └──┘             
325  @gpow_bit1 (multiplicative β) _
id    └───────┘  └────────────┘ 
src   └───────┘  └────────────┘
typ   └───────┘  └────────────┘ 
326  
327  theorem gsmul_neg (a : β) (n : ℤ) : gsmul n (- a) = - gsmul n a :=
id                                     └───┘        └───┘  
src                                     └───┘          └───┘
typ                                    └───┘        └───┘  
328  begin
st   └─────
329    induction n using int.induction_on with z ih z ih,
id               
src    └────────┘ └────────────────────────────────────┘
typ    └────────┘└────────────────────────────────────┘
doc    └────────┘ └────────────────────────────────────┘
txt    └────────┘ └────────────────────────────────────┘
par    └────────┘ └────────────────────────────────────┘
pid              └─────────────────────┘└─────────────┘
st   ──────────────────────────────────────────────────┘└─
330    { simp },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
331    { rw [add_comm] {occs := occurrences.pos [1]}, simp [add_gsmul, ih, -add_comm] },
id           └──────┘           └─────────────┘           └───────┘  └┘
src      └──┘└──────┘└┘ └──────┘└─────────────┘  └────┘└───────┘└┘  └───────────┘
typ      └──┘└──────┘└┘ └──────┘└─────────────┘  └────┘└───────┘└┘└┘└───────────┘
doc      └──┘        └┘ └──────┘                   └────┘         └┘  └───────────┘
txt      └──┘        └┘ └──────┘                   └────┘         └┘  └───────────┘
par      └──┘        └┘ └──────┘                   └────┘         └┘  └───────────┘
pid        └┘         └──────┘                                └┘  └──────────┘
st   ───┘└──────────┘└────────────────────────────┘└────────────────────────────────┘└┘
332    { rw [sub_eq_add_neg, add_comm] {occs := occurrences.pos [1]},
id           └────────────┘  └──────┘           └─────────────┘  
src      └──┘└────────────┘└┘└──────┘└┘ └──────┘└─────────────┘
typ      └──┘└────────────┘└┘└──────┘└┘ └──────┘└─────────────┘
doc      └──┘              └┘        └┘ └──────┘                 
txt      └──┘              └┘        └┘ └──────┘                 
par      └──┘              └┘        └┘ └──────┘                 
pid        └┘              └┘         └──────┘                 
st   ─────────────────────┘└────────┘└────────────────────────────┘└─
333      simp [ih, add_gsmul, neg_gsmul, -add_comm] }
id             └┘  └───────┘  └───────┘
src      └────┘  └┘└───────┘└┘└───────┘└───────────┘
typ      └────┘└┘└┘└───────┘└┘└───────┘└───────────┘
doc      └────┘  └┘         └┘         └───────────┘
txt      └────┘  └┘         └┘         └───────────┘
par      └────┘  └┘         └┘         └───────────┘
pid            └┘         └┘         └──────────┘
st   ──────────────────────────────────────────────┘└─
334  end
st   ──┘
335  
336  end group
337  
338  namespace is_group_hom
339  variables {β : Type v} [group α] [group β] (f : α → β) [is_group_hom f]
id                           └───┘     └───┘                 └──────────┘
src                          └───┘     └───┘                 └──────────┘
typ                          └───┘     └───┘                 └──────────┘
doc                                                          └──────────┘
340  
341  theorem map_pow (a : α) (n : ℕ) : f (a ^ n) = f a ^ n :=
id                                             
src                                                 
typ                                            
342  is_monoid_hom.map_pow f a n
id   └───────────────────┘   
src  └───────────────────┘
typ  └───────────────────┘   
343  
344  theorem map_gpow (a : α) (n : ℤ) : f (a ^ n) = f a ^ n :=
id                                              
src                                                  
typ                                             
345  by cases n; [exact is_group_hom.map_pow f _ _,
id                    └──────────────────┘ 
src     └────┘   └────┘└──────────────────┘ └──┘
typ     └────┘  └────┘└──────────────────┘└──┘
doc     └────┘    └────┘                     └──┘
txt     └────┘    └────┘                     └──┘
par     └────┘    └────┘                     └──┘
pid                                        └──┘
st     └────────────────────────────────────────────
346    exact (is_group_hom.map_inv f _).trans (congr_arg _ $ is_group_hom.map_pow f _ _)]
id            └──────────────────┘             └───────┘     └──────────────────┘ 
src    └────┘ └──────────────────┘ └────────┘ └───────┘└─┘ └──────────────────┘ └───┘
typ    └────┘ └──────────────────┘ └────────┘ └───────┘└─┘ └──────────────────┘└───┘
doc    └────┘ └──────────────────┘ └────────┘          └─┘                      └───┘
txt    └────┘                      └────────┘          └─┘                      └───┘
par    └────┘                      └────────┘          └─┘                      └───┘
pid                               └────────┘          └─┘                      └───┘
st   ───────────────────────────────────────────────────────────────────────────────────┘
347  
348  end is_group_hom
349  
350  namespace is_add_group_hom
351  variables {β : Type v} [add_group α] [add_group β] (f : α → β) [is_add_group_hom f]
id                           └───────┘     └───────┘                 └──────────────┘
src                          └───────┘     └───────┘                 └──────────────┘
typ                          └───────┘     └───────┘                 └──────────────┘
doc                                                                  └──────────────┘
352  
353  theorem map_smul (a : α) (n : ℕ) : f (n • a) = n • f a :=
id                                              
src                                                
typ                                             
354  is_add_monoid_hom.map_smul f a n
id   └────────────────────────┘   
src  └────────────────────────┘
typ  └────────────────────────┘   
355  
356  theorem map_gsmul (a : α) (n : ℤ) : f (gsmul n a) = gsmul n (f a) :=
id                                       └───┘     └───┘    
src                                        └───┘       └───┘
typ                                      └───┘     └───┘    
357  @is_group_hom.map_gpow (multiplicative α) (multiplicative β) _ _ f _ a n
id    └───────────────────┘  └────────────┘    └────────────┘           
src   └───────────────────┘  └────────────┘     └────────────┘
typ   └───────────────────┘  └────────────┘    └────────────┘           
358  
359  end is_add_group_hom
360  
361  namespace monoid_hom
362  variables {β : Type v} [group α] [group β] (f : α →* β)
id                           └───┘     └───┘           └┘
src                          └───┘     └───┘           └┘
typ                          └───┘     └───┘           └┘
doc                                                    └┘
363  
364  @[simp] theorem map_gpow (a : α) (n : ℤ) : f (a ^ n) = f a ^ n :=
id                                                      
src                                                          
typ                                                     
doc    └──┘
365  by cases n; [exact f.map_pow _ _,
id                    └───────┘
src     └────┘   └────┘└───────┘└──┘
typ     └────┘  └────┘└───────┘└──┘
doc     └────┘    └────┘         └──┘
txt     └────┘    └────┘         └──┘
par     └────┘    └────┘         └──┘
pid                            └──┘
st     └───────────────────────────────
366    exact (f.map_inv _).trans (congr_arg _ $ f.map_pow _ _)]
id            └───────┘           └───────┘     └───────┘
src    └────┘ └───────┘└────────┘ └───────┘└─┘ └───────┘└───┘
typ    └────┘ └───────┘└────────┘ └───────┘└─┘ └───────┘└───┘
doc    └────┘ └───────┘└────────┘          └─┘          └───┘
txt    └────┘          └────────┘          └─┘          └───┘
par    └────┘          └────────┘          └─┘          └───┘
pid                   └────────┘          └─┘          └───┘
st   ─────────────────────────────────────────────────────────┘
367  
368  end monoid_hom
369  
370  namespace add_monoid_hom
371  variables {β : Type v} [add_group α] [add_group β] (f : α →+ β)
id                           └───────┘     └───────┘           └┘
src                          └───────┘     └───────┘           └┘
typ                          └───────┘     └───────┘           └┘
doc                                                            └┘
372  
373  @[simp] theorem map_gsmul (a : α) (n : ℤ) : f (gsmul n a) = gsmul n (f a) :=
id                                               └───┘     └───┘    
src                                                └───┘       └───┘
typ                                              └───┘     └───┘    
doc    └──┘
374  by cases n; [exact f.map_smul _ _,
id                    └────────┘
src     └────┘   └────┘└────────┘└──┘
typ     └────┘  └────┘└────────┘└──┘
doc     └────┘    └────┘          └──┘
txt     └────┘    └────┘          └──┘
par     └────┘    └────┘          └──┘
pid                             └──┘
st     └────────────────────────────────
375    exact (f.map_neg _).trans (congr_arg _ $ f.map_smul _ _)]
id            └───────┘           └───────┘     └────────┘
src    └────┘ └───────┘└────────┘ └───────┘└─┘ └────────┘└───┘
typ    └────┘ └───────┘└────────┘ └───────┘└─┘ └────────┘└───┘
doc    └────┘          └────────┘          └─┘           └───┘
txt    └────┘          └────────┘          └─┘           └───┘
par    └────┘          └────────┘          └─┘           └───┘
pid                   └────────┘          └─┘           └───┘
st   ──────────────────────────────────────────────────────────┘
376  
377  end add_monoid_hom
378  local infix ` •ℤ `:70 := gsmul
id                            └───┘
src                           └───┘
typ                           └───┘
379  open_locale smul
380  
381  section comm_monoid
382  variables [comm_group α] {β : Type*} [add_comm_group β]
id              └────────┘                 └────────────┘
src             └────────┘                 └────────────┘
typ             └────────┘                 └────────────┘
383  
384  theorem mul_gpow (a b : α) : ∀ n:ℤ, (a * b)^n = a^n * b^n
id                                            
src                                                   
typ                                           
385  | (n : ℕ) := mul_pow a b n
id              └─────┘  
src              └─────┘
typ             └─────┘  
386  | -[1+ n] := show _⁻¹=_⁻¹*_⁻¹, by rw [mul_pow, mul_inv_rev, mul_comm]
id     └──┘            └┘ └┘ └┘         └─────┘  └─────────┘  └──────┘
src    └──┘            └┘ └┘ └┘     └──┘└─────┘└┘└─────────┘└┘└──────┘└┘
typ    └──┘            └┘ └┘ └┘     └──┘└─────┘└┘└─────────┘└┘└──────┘└┘
doc                                    └──┘       └┘           └┘        └┘
txt                                    └──┘       └┘           └┘        └┘
par                                    └──┘       └┘           └┘        └┘
pid                                      └┘       └┘           └┘        
st                                    └──────────┘└───────────┘└────────┘
387  theorem gsmul_add : ∀ (a b : β) (n : ℤ), n •ℤ (a + b) = n •ℤ a + n •ℤ b :=
id                                           └┘        └┘    └┘ 
src                                            └┘           └┘      └┘
typ                                          └┘        └┘    └┘ 
388  @mul_gpow (multiplicative β) _
id    └──────┘  └────────────┘ 
src   └──────┘  └────────────┘
typ   └──────┘  └────────────┘ 
389  
390  theorem gsmul_sub : ∀ (a b : β) (n : ℤ), gsmul n (a - b) = gsmul n a - gsmul n b :=
id                                          └───┘        └───┘    └───┘  
src                                          └───┘           └───┘      └───┘
typ                                         └───┘        └───┘    └───┘  
391  by simp [gsmul_add, gsmul_neg]
id            └───────┘  └───────┘
src     └────┘└───────┘└┘└───────┘└─
typ     └────┘└───────┘└┘└───────┘└─
doc     └────┘         └┘         └─
txt     └────┘         └┘         └─
par     └────┘         └┘         └─
pid                  └┘         
st     └────────────────────────────
392  
src  
typ  
doc  
txt  
par  
pid  
st   
393  instance gpow.is_group_hom (n : ℤ) : is_group_hom ((^ n) : α → α) :=
id                                       └──────────┘           
src                                      └──────────┘  
typ                                      └──────────┘           
doc                                       └──────────┘
394  { map_mul := λ _ _, mul_gpow _ _ n }
id                     └──────┘     
src                      └──────┘
typ                    └──────┘     
395  
396  instance gsmul.is_add_group_hom (n : ℤ) : is_add_group_hom (gsmul n : β → β) :=
id                                            └──────────────┘  └───┘       
src                                           └──────────────┘  └───┘
typ                                           └──────────────┘  └───┘       
doc                                            └──────────────┘
397  { map_add := λ _ _, gsmul_add _ _ n }
id                     └───────┘     
src                      └───────┘
typ                    └───────┘     
398  
399  end comm_monoid
400  
401  section group
402  
403  @[instance]
404  theorem is_add_group_hom.gsmul
405    {α β} [add_group α] [add_comm_group β] (f : α → β) [is_add_group_hom f] (z : ℤ) :
id            └───────┘    └────────────┘              └──────────────┘        
src           └───────┘     └────────────┘                 └──────────────┘         
typ           └───────┘    └────────────┘              └──────────────┘        
doc                                                        └──────────────┘
406    is_add_group_hom (λa, gsmul z (f a)) :=
id     └──────────────┘     └───┘    
src    └──────────────┘      └───┘
typ    └──────────────┘     └───┘    
doc    └──────────────┘
407  { map_add := assume a b, by rw [is_add_hom.map_add f, gsmul_add] }
id                                 └────────────────┘   └───────┘
src                              └──┘└────────────────┘ └┘└───────┘└┘
typ                            └──┘└────────────────┘└┘└───────┘└┘
doc                              └──┘                   └┘         └┘
txt                              └──┘                   └┘         └┘
par                              └──┘                   └┘         └┘
pid                                └┘                   └┘         
st                              └───────────────────────┘└─────────┘
408  
409  end group
410  
411  @[simp] lemma with_bot.coe_smul [add_monoid α] (a : α) (n : ℕ) :
id                                    └────────┘               
src                                   └────────┘                 
typ                                   └────────┘               
doc    └──┘
412    ((add_monoid.smul n a : α) : with_bot α) = add_monoid.smul n a :=
id       └─────────────┘         └──────┘    └─────────────┘  
src      └─────────────┘            └──────┘     └─────────────┘
typ      └─────────────┘         └──────┘    └─────────────┘  
413  by induction n; simp [*, succ_smul]; refl
id                           └───────┘
src     └────────┘   └───────┘└───────┘  └────
typ     └────────┘  └───────┘└───────┘  └────
doc     └────────┘   └───────┘           └────
txt     └────────┘   └───────┘           └────
par     └────────┘   └───────┘           └────
pid                     └──┘               
st     └───────────────────────────────────────
414  
src  
typ  
doc  
txt  
par  
pid  
st   
415  theorem add_monoid.smul_eq_mul' [semiring α] (a : α) (n : ℕ) : n • a = a * n :=
id                                    └──────┘                         
src                                   └──────┘                             
typ                                   └──────┘                         
416  by induction n with n ih; [rw [add_monoid.zero_smul, nat.cast_zero, mul_zero],
id                                └──────────────────┘  └───────────┘  └──────┘
src     └────────┘ └────────┘  └──┘└──────────────────┘└┘└───────────┘└┘└──────┘
typ     └────────┘└────────┘  └──┘└──────────────────┘└┘└───────────┘└┘└──────┘
doc     └────────┘ └────────┘   └──┘                    └┘             └┘        
txt     └────────┘ └────────┘   └──┘                    └┘             └┘        
par     └────────┘ └────────┘   └──┘                    └┘             └┘        
pid               └───────┘     └┘                    └┘             └┘        
st     └───────────────────────────┘└──────────────────┘└─────────────┘└────────┘└─
417    rw [succ_smul', ih, nat.cast_succ, mul_add, mul_one]]
id         └────────┘  └┘  └───────────┘  └─────┘  └─────┘
src    └──┘└────────┘└┘  └┘└───────────┘└┘└─────┘└┘└─────┘
typ    └──┘└────────┘└┘└┘└┘└───────────┘└┘└─────┘└┘└─────┘
doc    └──┘          └┘  └┘             └┘       └┘       
txt    └──┘          └┘  └┘             └┘       └┘       
par    └──┘          └┘  └┘             └┘       └┘       
pid      └┘          └┘  └┘             └┘       └┘       
st   ─────┘└────────┘└──┘└─────────────┘└───────┘└───────┘
418  
419  theorem add_monoid.smul_eq_mul [semiring α] (n : ℕ) (a : α) : n • a = n * a :=
id                                   └──────┘                         
src                                  └──────┘                             
typ                                  └──────┘                         
420  by rw [add_monoid.smul_eq_mul', nat.mul_cast_comm]
id          └─────────────────────┘  └───────────────┘
src     └──┘└─────────────────────┘└┘└───────────────┘└─
typ     └──┘└─────────────────────┘└┘└───────────────┘└─
doc     └──┘                       └┘                 └─
txt     └──┘                       └┘                 └─
par     └──┘                       └┘                 └─
pid       └┘                       └┘                 
st     └──────────────────────────┘└─────────────────┘
421  
src  
typ  
doc  
txt  
par  
pid  
st   
422  theorem add_monoid.mul_smul_left [semiring α] (a b : α) (n : ℕ) : n • (a * b) = a * (n • b) :=
id                                     └──────┘                                  
src                                    └──────┘                                        
typ                                    └──────┘                                  
423  by rw [add_monoid.smul_eq_mul', add_monoid.smul_eq_mul', mul_assoc]
id          └─────────────────────┘  └─────────────────────┘  └───────┘
src     └──┘└─────────────────────┘└┘└─────────────────────┘└┘└───────┘└─
typ     └──┘└─────────────────────┘└┘└─────────────────────┘└┘└───────┘└─
doc     └──┘                       └┘                       └┘         └─
txt     └──┘                       └┘                       └┘         └─
par     └──┘                       └┘                       └┘         └─
pid       └┘                       └┘                       └┘         
st     └──────────────────────────┘└───────────────────────┘└─────────┘
424  
src  
typ  
doc  
txt  
par  
pid  
st   
425  theorem add_monoid.mul_smul_assoc [semiring α] (a b : α) (n : ℕ) : n • (a * b) = n • a * b :=
id                                      └──────┘                                 
src                                     └──────┘                                       
typ                                     └──────┘                                 
426  by rw [add_monoid.smul_eq_mul, add_monoid.smul_eq_mul, mul_assoc]
id          └────────────────────┘  └────────────────────┘  └───────┘
src     └──┘└────────────────────┘└┘└────────────────────┘└┘└───────┘└─
typ     └──┘└────────────────────┘└┘└────────────────────┘└┘└───────┘└─
doc     └──┘                      └┘                      └┘         └─
txt     └──┘                      └┘                      └┘         └─
par     └──┘                      └┘                      └┘         └─
pid       └┘                      └┘                      └┘         
st     └─────────────────────────┘└──────────────────────┘└─────────┘
427  
src  
typ  
doc  
txt  
par  
pid  
st   
428  lemma zero_pow [semiring α] : ∀ {n : ℕ}, 0 < n → (0 : α) ^ n = 0
id                   └──────┘                             
src                  └──────┘                                  
typ                  └──────┘                             
429  | (n+1) _ := zero_mul _
id               └──────┘
src              └──────┘
typ              └──────┘
430  
431  @[simp, move_cast] theorem nat.cast_pow [semiring α] (n m : ℕ) : (↑(n ^ m) : α) = ↑n ^ m :=
id                                            └──────┘                           
src                                           └──────┘                               
typ                                           └──────┘                           
doc    └──┘  └───────┘
432  by induction m with m ih; [exact nat.cast_one, rw [nat.pow_succ, pow_succ', nat.cast_mul, ih]]
id                                  └──────────┘      └──────────┘  └───────┘  └──────────┘  └┘
src     └────────┘ └────────┘  └────┘└──────────┘  └──┘└──────────┘└┘└───────┘└┘└──────────┘└┘  
typ     └────────┘└────────┘  └────┘└──────────┘  └──┘└──────────┘└┘└───────┘└┘└──────────┘└┘└┘
doc     └────────┘ └────────┘   └────┘              └──┘            └┘         └┘            └┘  
txt     └────────┘ └────────┘   └────┘              └──┘            └┘         └┘            └┘  
par     └────────┘ └────────┘   └────┘              └──┘            └┘         └┘            └┘  
pid               └───────┘                        └┘            └┘         └┘            └┘  
st     └───────────────────────────────────────────────┘└──────────┘└─────────┘└────────────┘└──┘
433  
434  @[simp, move_cast] theorem int.coe_nat_pow (n m : ℕ) : ((n ^ m : ℕ) : ℤ) = n ^ m :=
id                                                                         
src                                                                          
typ                                                                        
doc    └──┘  └───────┘
435  by induction m with m ih; [exact int.coe_nat_one, rw [nat.pow_succ, pow_succ', int.coe_nat_mul, ih]]
id                                  └─────────────┘      └──────────┘  └───────┘  └─────────────┘  └┘
src     └────────┘ └────────┘  └────┘└─────────────┘  └──┘└──────────┘└┘└───────┘└┘└─────────────┘└┘  
typ     └────────┘└────────┘  └────┘└─────────────┘  └──┘└──────────┘└┘└───────┘└┘└─────────────┘└┘└┘
doc     └────────┘ └────────┘   └────┘                 └──┘            └┘         └┘               └┘  
txt     └────────┘ └────────┘   └────┘                 └──┘            └┘         └┘               └┘  
par     └────────┘ └────────┘   └────┘                 └──┘            └┘         └┘               └┘  
pid               └───────┘                           └┘            └┘         └┘               └┘  
st     └──────────────────────────────────────────────────┘└──────────┘└─────────┘└───────────────┘└──┘
436  
437  theorem int.nat_abs_pow (n : ℤ) (k : ℕ) : int.nat_abs (n ^ k) = (int.nat_abs n) ^ k :=
id                                           └─────────┘        └─────────┘    
src                                          └─────────┘          └─────────┘    
typ                                          └─────────┘        └─────────┘    
438  by induction k with k ih; [refl, rw [pow_succ', int.nat_abs_mul, nat.pow_succ, ih]]
id                                      └───────┘  └─────────────┘  └──────────┘  └┘
src     └────────┘ └────────┘  └──┘  └──┘└───────┘└┘└─────────────┘└┘└──────────┘└┘  
typ     └────────┘└────────┘  └──┘  └──┘└───────┘└┘└─────────────┘└┘└──────────┘└┘└┘
doc     └────────┘ └────────┘   └──┘  └──┘         └┘               └┘            └┘  
txt     └────────┘ └────────┘   └──┘  └──┘         └┘               └┘            └┘  
par     └────────┘ └────────┘   └──┘  └──┘         └┘               └┘            └┘  
pid               └───────┘           └┘         └┘               └┘            └┘  
st     └─────────────────────────────────┘└───────┘└───────────────┘└────────────┘└──┘
439  
440  theorem is_semiring_hom.map_pow {β} [semiring α] [semiring β]
id                                        └──────┘    └──────┘ 
src                                       └──────┘     └──────┘
typ                                       └──────┘    └──────┘ 
441    (f : α → β) [is_semiring_hom f] (x : α) (n : ℕ) : f (x ^ n) = f x ^ n :=
id                └─────────────┘                             
src                 └─────────────┘                                   
typ               └─────────────┘                             
doc                 └─────────────┘
442  by induction n with n ih; [exact is_semiring_hom.map_one f,
id                                  └─────────────────────┘ 
src     └────────┘ └────────┘  └────┘└─────────────────────┘
typ     └────────┘└────────┘  └────┘└─────────────────────┘
doc     └────────┘ └────────┘   └────┘                       
txt     └────────┘ └────────┘   └────┘                       
par     └────────┘ └────────┘   └────┘                       
pid               └───────┘                               
st     └─────────────────────────────────────────────────────────
443    rw [pow_succ, pow_succ, is_semiring_hom.map_mul f, ih]]
id         └──────┘  └──────┘  └─────────────────────┘   └┘
src    └──┘└──────┘└┘└──────┘└┘└─────────────────────┘ └┘  
typ    └──┘└──────┘└┘└──────┘└┘└─────────────────────┘└┘└┘
doc    └──┘        └┘        └┘                        └┘  
txt    └──┘        └┘        └┘                        └┘  
par    └──┘        └┘        └┘                        └┘  
pid      └┘        └┘        └┘                        └┘  
st   ─────┘└──────┘└────────┘└─────────────────────────┘└──┘
444  
445  @[simp] lemma ring_hom.map_pow {β} [semiring α] [semiring β] (f : α →+* β) (a) :
id                                       └──────┘    └──────┘         └─┘ 
src                                      └──────┘     └──────┘           └─┘
typ                                      └──────┘    └──────┘         └─┘ 
doc    └──┘                                                              └─┘
446    ∀ n : ℕ, f (a ^ n) = (f a) ^ n :=
id                         
src                            
typ                        
447  monoid_hom.map_pow f.to_monoid_hom a
id   └────────────────┘ └────────────┘ 
src  └────────────────┘  └────────────┘
typ  └────────────────┘ └────────────┘ 
448  
449  theorem neg_one_pow_eq_or {R} [ring R] : ∀ n : ℕ, (-1 : R)^n = 1 ∨ (-1 : R)^n = -1
id                                  └──┘                               
src                                 └──┘                                     
typ                                 └──┘                               
450  | 0     := or.inl rfl
id              └────┘ └─┘
src             └────┘ └─┘
typ             └────┘ └─┘
451  | (n+1) := (neg_one_pow_eq_or n).swap.imp
id             └───────────────┘   └──┘ └─┘
src                                 └──┘ └─┘
typ            └───────────────┘   └──┘ └─┘
452    (λ h, by rw [pow_succ, h, neg_one_mul, neg_neg])
id                 └──────┘    └─────────┘  └─────┘
src             └──┘└──────┘└┘ └┘└─────────┘└┘└─────┘
typ            └──┘└──────┘└┘└┘└─────────┘└┘└─────┘
doc             └──┘        └┘ └┘└─────────┘└┘       
txt             └──┘        └┘ └┘           └┘       
par             └──┘        └┘ └┘           └┘       
pid               └┘        └┘ └┘           └┘       
st             └───────────┘└─┘└───────────┘└───────┘
453    (λ h, by rw [pow_succ, h, mul_one])
id                 └──────┘    └─────┘
src             └──┘└──────┘└┘ └┘└─────┘
typ            └──┘└──────┘└┘└┘└─────┘
doc             └──┘        └┘ └┘       
txt             └──┘        └┘ └┘       
par             └──┘        └┘ └┘       
pid               └┘        └┘ └┘       
st             └───────────┘└─┘└───────┘
454  
455  lemma pow_dvd_pow [comm_semiring α] (a : α) {m n : ℕ} (h : m ≤ n) :
id                      └───────────┘                          
src                     └───────────┘                            
typ                     └───────────┘                          
456    a ^ m ∣ a ^ n := ⟨a ^ (n - m), by rw [← pow_add, nat.add_sub_cancel' h]⟩
id                                 └─────┘  └─────────────────┘ 
src                                 └────┘└─────┘└┘└─────────────────┘ 
typ                          └────┘└─────┘└┘└─────────────────┘
doc                                      └────┘       └┘                    
txt                                      └────┘       └┘                    
par                                      └────┘       └┘                    
pid                                        └──┘       └┘                    
st                                      └────────────┘└─────────────────────┘
457  
458  theorem gsmul_eq_mul [ring α] (a : α) : ∀ n, n •ℤ a = n * a
id                         └──┘                 └┘     
src                        └──┘                     └┘      
typ                        └──┘                 └┘     
459  | (n : ℕ) := add_monoid.smul_eq_mul _ _
id               └────────────────────┘
src              └────────────────────┘
typ              └────────────────────┘
460  | -[1+ n] := show -(_•_)=-_*_, by rw [neg_mul_eq_neg_mul_symm, add_monoid.smul_eq_mul, nat.cast_succ]
id     └──┘                          └─────────────────────┘  └────────────────────┘  └───────────┘
src    └──┘                      └──┘└─────────────────────┘└┘└────────────────────┘└┘└───────────┘└─
typ    └──┘                      └──┘└─────────────────────┘└┘└────────────────────┘└┘└───────────┘└─
doc                                    └──┘                       └┘                      └┘             └─
txt                                    └──┘                       └┘                      └┘             └─
par                                    └──┘                       └┘                      └┘             └─
pid                                      └┘                       └┘                      └┘             
st                                    └──────────────────────────┘└──────────────────────┘└─────────────┘
461  
src  
typ  
doc  
txt  
par  
pid  
st   
462  theorem gsmul_eq_mul' [ring α] (a : α) (n : ℤ) : n •ℤ a = a * n :=
id                          └──┘                    └┘     
src                         └──┘                       └┘      
typ                         └──┘                    └┘     
463  by rw [gsmul_eq_mul, int.mul_cast_comm]
id          └──────────┘  └───────────────┘
src     └──┘└──────────┘└┘└───────────────┘└─
typ     └──┘└──────────┘└┘└───────────────┘└─
doc     └──┘            └┘                 └─
txt     └──┘            └┘                 └─
par     └──┘            └┘                 └─
pid       └┘            └┘                 
st     └───────────────┘└─────────────────┘
464  
src  
typ  
doc  
txt  
par  
pid  
st   
465  theorem mul_gsmul_left [ring α] (a b : α) (n : ℤ) : n •ℤ (a * b) = a * (n •ℤ b) :=
id                           └──┘                      └┘           └┘ 
src                          └──┘                         └┘               └┘
typ                          └──┘                      └┘           └┘ 
466  by rw [gsmul_eq_mul', gsmul_eq_mul', mul_assoc]
id          └───────────┘  └───────────┘  └───────┘
src     └──┘└───────────┘└┘└───────────┘└┘└───────┘└─
typ     └──┘└───────────┘└┘└───────────┘└┘└───────┘└─
doc     └──┘             └┘             └┘         └─
txt     └──┘             └┘             └┘         └─
par     └──┘             └┘             └┘         └─
pid       └┘             └┘             └┘         
st     └────────────────┘└─────────────┘└─────────┘
467  
src  
typ  
doc  
txt  
par  
pid  
st   
468  theorem mul_gsmul_assoc [ring α] (a b : α) (n : ℤ) : n •ℤ (a * b) = n •ℤ a * b :=
id                            └──┘                      └┘        └┘   
src                           └──┘                         └┘           └┘   
typ                           └──┘                      └┘        └┘   
469  by rw [gsmul_eq_mul, gsmul_eq_mul, mul_assoc]
id          └──────────┘  └──────────┘  └───────┘
src     └──┘└──────────┘└┘└──────────┘└┘└───────┘└─
typ     └──┘└──────────┘└┘└──────────┘└┘└───────┘└─
doc     └──┘            └┘            └┘         └─
txt     └──┘            └┘            └┘         └─
par     └──┘            └┘            └┘         └─
pid       └┘            └┘            └┘         
st     └───────────────┘└────────────┘└─────────┘
470  
src  
typ  
doc  
txt  
par  
pid  
st   
471  @[simp, move_cast] theorem int.cast_pow [ring α] (n : ℤ) (m : ℕ) : (↑(n ^ m) : α) = ↑n ^ m :=
id                                            └──┘                                
src                                           └──┘                                    
typ                                           └──┘                                
doc    └──┘  └───────┘
472  by induction m with m ih; [exact int.cast_one,
id                                  └──────────┘
src     └────────┘ └────────┘  └────┘└──────────┘
typ     └────────┘└────────┘  └────┘└──────────┘
doc     └────────┘ └────────┘   └────┘
txt     └────────┘ └────────┘   └────┘
par     └────────┘ └────────┘   └────┘
pid               └───────┘        
st     └────────────────────────────────────────────
473    rw [pow_succ, pow_succ, int.cast_mul, ih]]
id         └──────┘  └──────┘  └──────────┘  └┘
src    └──┘└──────┘└┘└──────┘└┘└──────────┘└┘  
typ    └──┘└──────┘└┘└──────┘└┘└──────────┘└┘└┘
doc    └──┘        └┘        └┘            └┘  
txt    └──┘        └┘        └┘            └┘  
par    └──┘        └┘        └┘            └┘  
pid      └┘        └┘        └┘            └┘  
st   ─────┘└──────┘└────────┘└────────────┘└──┘
474  
475  lemma neg_one_pow_eq_pow_mod_two [ring α] {n : ℕ} : (-1 : α) ^ n = -1 ^ (n % 2) :=
id                                     └──┘                           
src                                    └──┘                               
typ                                    └──┘                           
476  by rw [← nat.mod_add_div n 2, pow_add, pow_mul]; simp [pow_two]
id            └─────────────┘     └─────┘  └─────┘         └─────┘
src     └────┘└─────────────┘ └──┘└─────┘└┘└─────┘  └────┘└─────┘└─
typ     └────┘└─────────────┘└──┘└─────┘└┘└─────┘  └────┘└─────┘└─
doc     └────┘                └──┘       └┘         └────┘       └─
txt     └────┘                └──┘       └┘         └────┘       └─
par     └────┘                └──┘       └┘         └────┘       └─
pid       └──┘                └──┘       └┘                    
st     └───────────────────────┘└────────┘└───────┘└────────────────
477  
src  
typ  
doc  
txt  
par  
pid  
st   
478  theorem sq_sub_sq [comm_ring α] (a b : α) : a ^ 2 - b ^ 2 = (a + b) * (a - b) :=
id                      └───────┘                                 
src                     └───────┘                                       
typ                     └───────┘                                 
479  by rw [pow_two, pow_two, mul_self_sub_mul_self]
id          └─────┘  └─────┘  └───────────────────┘
src     └──┘└─────┘└┘└─────┘└┘└───────────────────┘└─
typ     └──┘└─────┘└┘└─────┘└┘└───────────────────┘└─
doc     └──┘       └┘       └┘└───────────────────┘└─
txt     └──┘       └┘       └┘                     └─
par     └──┘       └┘       └┘                     └─
pid       └┘       └┘       └┘                     
st     └──────────┘└───────┘└─────────────────────┘
480  
src  
typ  
doc  
txt  
par  
pid  
st   
481  theorem pow_eq_zero [domain α] {x : α} {n : ℕ} (H : x^n = 0) : x = 0 :=
id                        └────┘                              
src                       └────┘                                   
typ                       └────┘                              
doc                       └────┘
482  begin
st   └─────
483    induction n with n ih,
id               
src    └────────┘ └────────┘
typ    └────────┘└────────┘
doc    └────────┘ └────────┘
txt    └────────┘ └────────┘
par    └────────┘ └────────┘
pid              └───────┘
st   ──────────────────────┘└─
484    { rw pow_zero at H,
id          └──────┘
src      └─┘└──────┘└───┘
typ      └─┘└──────┘└───┘
doc      └─┘        └───┘
txt      └─┘        └───┘
par      └─┘        └───┘
pid                └───┘
st   ───┘└──────────────┘└─
485      rw [← mul_one x, H, mul_zero] },
id             └─────┘     └──────┘
src      └────┘└─────┘ └┘ └┘└──────┘└┘
typ      └────┘└─────┘└┘└┘└──────┘└┘
doc      └────┘        └┘ └┘        └┘
txt      └────┘        └┘ └┘        └┘
par      └────┘        └┘ └┘        └┘
pid        └──┘        └┘ └┘        
st   ──────────────────┘└─┘└────────┘└┘
486    exact or.cases_on (mul_eq_zero.1 H) id ih
id           └─────────┘  └─────────┘     └┘ └┘
src    └────┘└─────────┘ └─────────┘└─┘ └┘└┘  
typ    └────┘└─────────┘ └─────────┘└─┘└┘└┘└┘
doc    └────┘            └─────────┘└─┘ └┘    
txt    └────┘                       └─┘ └┘    
par    └────┘                       └─┘ └┘    
pid                                └─┘ └┘    
st   ───────────────────────────────────────────┘
487  end
st   └─┘
488  
489  @[field_simps] theorem pow_ne_zero [domain α] {a : α} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
id                                       └────┘                                
src                                      └────┘                                     
typ                                      └────┘                                
doc    └─────────┘                       └────┘
490  mt pow_eq_zero h
id   └┘ └─────────┘ 
src  └┘ └─────────┘
typ  └┘ └─────────┘ 
491  
492  @[simp] theorem one_div_pow [division_ring α] {a : α} (ha : a ≠ 0) (n : ℕ) : (1 / a) ^ n = 1 / a ^ n :=
id                                └───────────┘                                            
src                               └───────────┘                                                 
typ                               └───────────┘                                            
doc    └──┘
493  by induction n with n ih; [exact (div_one _).symm,
id                                   └─────┘
src     └────────┘ └────────┘  └────┘ └─────┘└──────┘
typ     └────────┘└────────┘  └────┘ └─────┘└──────┘
doc     └────────┘ └────────┘   └────┘        └──────┘
txt     └────────┘ └────────┘   └────┘        └──────┘
par     └────────┘ └────────┘   └────┘        └──────┘
pid               └───────┘                └─────┘
st     └────────────────────────────────────────────────
494    rw [pow_succ', ih, division_ring.one_div_mul_one_div (pow_ne_zero _ ha) ha]]; refl
id         └───────┘  └┘  └───────────────────────────────┘  └─────────┘       └┘
src    └──┘└───────┘└┘  └┘└───────────────────────────────┘ └─────────┘└─┘  └┘     └────
typ    └──┘└───────┘└┘└┘└┘└───────────────────────────────┘ └─────────┘└─┘  └┘└┘   └────
doc    └──┘         └┘  └┘                                             └─┘  └┘     └────
txt    └──┘         └┘  └┘                                             └─┘  └┘     └────
par    └──┘         └┘  └┘                                             └─┘  └┘     └────
pid      └┘         └┘  └┘                                             └─┘  └┘         
st   ─────┘└───────┘└──┘└───────────────────────────────────────────────────────┘└───────
495  
src  
typ  
doc  
txt  
par  
pid  
st   
496  @[simp] theorem division_ring.inv_pow [division_ring α] {a : α} (ha : a ≠ 0) (n : ℕ) : a⁻¹ ^ n = (a ^ n)⁻¹ :=
id                                          └───────────┘                              └┘        └┘
src                                         └───────────┘                                  └┘           └┘
typ                                         └───────────┘                              └┘        └┘
doc    └──┘
497  by simpa only [inv_eq_one_div] using one_div_pow ha n
id                  └────────────┘        └─────────┘ └┘ 
src     └──────────┘└────────────┘└──────┘└─────────┘   
typ     └──────────┘└────────────┘└──────┘└─────────┘└┘
doc     └──────────┘              └──────┘              
txt     └──────────┘              └──────┘              
par     └──────────┘              └──────┘              
pid          └──┘└┘              └────┘              
st     └───────────────────────────────────────────────────
498  
src  
typ  
doc  
txt  
par  
pid  
st   
499  @[simp] theorem div_pow [field α] (a : α) {b : α} (hb : b ≠ 0) (n : ℕ) : (a / b) ^ n = a ^ n / b ^ n :=
id                            └───┘                                                   
src                           └───┘                                                            
typ                           └───┘                                                   
doc    └──┘
500  by rw [div_eq_mul_one_div, mul_pow, one_div_pow hb, ← div_eq_mul_one_div]
id          └────────────────┘  └─────┘  └─────────┘ └┘    └────────────────┘
src     └──┘└────────────────┘└┘└─────┘└┘└─────────┘  └──┘└────────────────┘└─
typ     └──┘└────────────────┘└┘└─────┘└┘└─────────┘└┘└──┘└────────────────┘└─
doc     └──┘                  └┘       └┘             └──┘                  └─
txt     └──┘                  └┘       └┘             └──┘                  └─
par     └──┘                  └┘       └┘             └──┘                  └─
pid       └┘                  └┘       └┘             └──┘                  
st     └─────────────────────┘└───────┘└──────────────┘└────────────────────┘
501  
src  
typ  
doc  
txt  
par  
pid  
st   
502  theorem add_monoid.smul_nonneg [ordered_comm_monoid α] {a : α} (H : 0 ≤ a) : ∀ n : ℕ, 0 ≤ n • a
id                                   └─────────────────┘                                  
src                                  └─────────────────┘                                      
typ                                  └─────────────────┘                                  
doc                                  └─────────────────┘
503  | 0     := le_refl _
id              └─────┘
src             └─────┘
typ             └─────┘
504  | (n+1) := add_nonneg' H (add_monoid.smul_nonneg n)
id            └─────────┘   └────────────────────┘
src            └─────────┘
typ           └─────────┘   └────────────────────┘
505  
506  lemma pow_abs [decidable_linear_ordered_comm_ring α] (a : α) (n : ℕ) : (abs a)^n = abs (a^n) :=
id                  └────────────────────────────────┘                    └─┘    └─┘  
src                 └────────────────────────────────┘                      └─┘      └─┘   
typ                 └────────────────────────────────┘                    └─┘    └─┘  
507  by induction n with n ih; [exact (abs_one).symm,
id                                   └─────┘
src     └────────┘ └────────┘  └────┘ └─────┘└────┘
typ     └────────┘└────────┘  └────┘ └─────┘└────┘
doc     └────────┘ └────────┘   └────┘        └────┘
txt     └────────┘ └────────┘   └────┘        └────┘
par     └────────┘ └────────┘   └────┘        └────┘
pid               └───────┘                └───┘
st     └──────────────────────────────────────────────
508    rw [pow_succ, pow_succ, ih, abs_mul]]
id         └──────┘  └──────┘  └┘  └─────┘
src    └──┘└──────┘└┘└──────┘└┘  └┘└─────┘
typ    └──┘└──────┘└┘└──────┘└┘└┘└┘└─────┘
doc    └──┘        └┘        └┘  └┘       
txt    └──┘        └┘        └┘  └┘       
par    └──┘        └┘        └┘  └┘       
pid      └┘        └┘        └┘  └┘       
st   ─────┘└──────┘└────────┘└──┘└───────┘
509  
510  lemma abs_neg_one_pow [decidable_linear_ordered_comm_ring α] (n : ℕ) : abs ((-1 : α)^n) = 1 :=
id                          └────────────────────────────────┘            └─┘          
src                         └────────────────────────────────┘             └─┘            
typ                         └────────────────────────────────┘            └─┘          
511  by rw [←pow_abs, abs_neg, abs_one, one_pow]
id           └─────┘  └─────┘  └─────┘  └─────┘
src     └───┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└─
typ     └───┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└─
doc     └───┘       └┘       └┘       └┘       └─
txt     └───┘       └┘       └┘       └┘       └─
par     └───┘       └┘       └┘       └┘       └─
pid       └─┘       └┘       └┘       └┘       
st     └───────────┘└───────┘└───────┘└───────┘
512  
src  
typ  
doc  
txt  
par  
pid  
st   
513  @[field_simps] lemma inv_pow' [discrete_field α] (a : α) (n : ℕ) : a⁻¹ ^ n = (a ^ n)⁻¹ :=
id                                  └────────────┘                   └┘        └┘
src                                 └────────────┘                      └┘           └┘
typ                                 └────────────┘                   └┘        └┘
doc    └─────────┘
514  by induction n; simp [*, pow_succ, mul_inv', mul_comm]
id                           └──────┘  └──────┘  └──────┘
src     └────────┘   └───────┘└──────┘└┘└──────┘└┘└──────┘└─
typ     └────────┘  └───────┘└──────┘└┘└──────┘└┘└──────┘└─
doc     └────────┘   └───────┘        └┘        └┘        └─
txt     └────────┘   └───────┘        └┘        └┘        └─
par     └────────┘   └───────┘        └┘        └┘        └─
pid                     └──┘        └┘        └┘        
st     └────────────────────────────────────────────────────
515  
src  
typ  
doc  
txt  
par  
pid  
st   
516  @[field_simps] lemma pow_div [discrete_field α] (a b : α) (n : ℕ) : (a / b)^n = a^n / b^n :=
id                                 └────────────┘                             
src                                └────────────┘                                     
typ                                └────────────┘                             
doc    └─────────┘
517  by simp [div_eq_mul_inv, mul_pow, inv_pow']
id            └────────────┘  └─────┘  └──────┘
src     └────┘└────────────┘└┘└─────┘└┘└──────┘└─
typ     └────┘└────────────┘└┘└─────┘└┘└──────┘└─
doc     └────┘              └┘       └┘        └─
txt     └────┘              └┘       └┘        └─
par     └────┘              └┘       └┘        └─
pid                       └┘       └┘        
st     └─────────────────────────────────────────
518  
src  
typ  
doc  
txt  
par  
pid  
st   
519  lemma pow_inv [division_ring α] (a : α) : ∀ n : ℕ, a ≠ 0 → (a^n)⁻¹ = (a⁻¹)^n
id                  └───────────┘                           └┘   └┘ 
src                 └───────────┘                                 └┘    └┘ 
typ                 └───────────┘                           └┘   └┘ 
520  | 0     ha := inv_one
id                 └─────┘
src                └─────┘
typ                └─────┘
521  | (n+1) ha := by rw [pow_succ, pow_succ', mul_inv_eq (pow_ne_zero _ ha) ha, pow_inv _ ha]
id                       └──────┘  └───────┘  └────────┘  └─────────┘       └┘  └─────┘   └┘
src                  └──┘└──────┘└┘└───────┘└┘└────────┘ └─────────┘└─┘  └┘  └┘       └─┘  └─
typ                  └──┘└──────┘└┘└───────┘└┘└────────┘ └─────────┘└─┘  └┘└┘└┘└─────┘└─┘└┘└─
doc                   └──┘        └┘         └┘                      └─┘  └┘  └┘       └─┘  └─
txt                   └──┘        └┘         └┘                      └─┘  └┘  └┘       └─┘  └─
par                   └──┘        └┘         └┘                      └─┘  └┘  └┘       └─┘  └─
pid                     └┘        └┘         └┘                      └─┘  └┘  └┘       └─┘  
st                   └───────────┘└─────────┘└────────────────────────────────┘└────────────┘
522  
src  
typ  
doc  
txt  
par  
pid  
st   
523  namespace add_monoid
524  variable [ordered_comm_monoid α]
id             └─────────────────┘
src            └─────────────────┘
typ            └─────────────────┘
doc            └─────────────────┘
525  
526  theorem smul_le_smul {a : α} {n m : ℕ} (ha : 0 ≤ a) (h : n ≤ m) : n • a ≤ m • a :=
id                                                                    
src                                                                         
typ                                                                   
527  let ⟨k, hk⟩ := nat.le.dest h in
id   └─┘           └─────────┘ 
src                 └─────────┘
typ  └─┘           └─────────┘ 
528  calc n • a = n • a + 0 : (add_zero _).symm
id                      └──────┘   └──┘
src                         └──────┘   └──┘
typ                     └──────┘   └──┘
529    ... ≤ n • a + k • a : add_le_add_left' (smul_nonneg ha _)
id                     └──────────────┘  └─────────┘ └┘
src                       └──────────────┘  └─────────┘
typ                    └──────────────┘  └─────────┘ └┘
530    ... = m • a : by rw [← hk, add_smul]
id                         └┘  └──────┘
src                    └────┘  └┘└──────┘└─
typ                  └────┘└┘└┘└──────┘└─
doc                     └────┘  └┘        └─
txt                     └────┘  └┘        └─
par                     └────┘  └┘        └─
pid                       └──┘  └┘        
st                     └───────┘└────────┘
531  
src  
typ  
doc  
txt  
par  
pid  
st   
532  lemma smul_le_smul_of_le_right {a b : α} (hab : a ≤ b) : ∀ i : ℕ, i • a ≤ i • b
id                                                                     
src                                                                          
typ                                                                    
533  | 0 := by simp
src            └───┘
typ            └───┘
doc            └───┘
txt            └───┘
par            └───┘
pid                
st            └────┘
534  | (k+1) := add_le_add' hab (smul_le_smul_of_le_right _)
id             └─────────┘ └─┘  └──────────────────────┘
src            └─────────┘
typ            └─────────┘ └─┘  └──────────────────────┘
535  
536  end add_monoid
537  
538  namespace canonically_ordered_semiring
539  variable [canonically_ordered_comm_semiring α]
id             └───────────────────────────────┘
src            └───────────────────────────────┘
typ            └───────────────────────────────┘
540  
541  theorem pow_pos {a : α} (H : 0 < a) : ∀ n : ℕ, 0 < a ^ n
id                                                  
src                                                    
typ                                                 
542  | 0     := canonically_ordered_semiring.zero_lt_one
id              └──────────────────────────────────────┘
src             └──────────────────────────────────────┘
typ             └──────────────────────────────────────┘
doc             └──────────────────────────────────────┘
543  | (n+1) := canonically_ordered_semiring.mul_pos.2 ⟨H, pow_pos n⟩
id            └──────────────────────────────────┘     └─────┘
src            └──────────────────────────────────┘
typ           └──────────────────────────────────┘     └─────┘
544  
545  lemma pow_le_pow_of_le_left {a b : α} (hab : a ≤ b) : ∀ i : ℕ, a^i ≤ b^i
id                                                              
src                                                                    
typ                                                             
546  | 0     := by simp
src                └───┘
typ                └───┘
doc                └───┘
txt                └───┘
par                └───┘
pid                    
st                └────┘
547  | (k+1) := canonically_ordered_semiring.mul_le_mul hab (pow_le_pow_of_le_left k)
id            └─────────────────────────────────────┘ └─┘  └───────────────────┘
src            └─────────────────────────────────────┘
typ           └─────────────────────────────────────┘ └─┘  └───────────────────┘
548  
549  theorem one_le_pow_of_one_le {a : α} (H : 1 ≤ a) (n : ℕ) : 1 ≤ a ^ n :=
id                                                               
src                                                                
typ                                                              
550  by simpa only [one_pow] using pow_le_pow_of_le_left H n
id                  └─────┘        └───────────────────┘  
src     └──────────┘└─────┘└──────┘└───────────────────┘  
typ     └──────────┘└─────┘└──────┘└───────────────────┘
doc     └──────────┘       └──────┘                       
txt     └──────────┘       └──────┘                       
par     └──────────┘       └──────┘                       
pid          └──┘└┘       └────┘                       
st     └─────────────────────────────────────────────────────
551  
src  
typ  
doc  
txt  
par  
pid  
st   
552  theorem pow_le_one {a : α} (H : a ≤ 1) (n : ℕ) : a ^ n ≤ 1:=
id                                                   
src                                                      
typ                                                  
553  by simpa only [one_pow] using pow_le_pow_of_le_left H n
id                  └─────┘        └───────────────────┘  
src     └──────────┘└─────┘└──────┘└───────────────────┘  
typ     └──────────┘└─────┘└──────┘└───────────────────┘
doc     └──────────┘       └──────┘                       
txt     └──────────┘       └──────┘                       
par     └──────────┘       └──────┘                       
pid          └──┘└┘       └────┘                       
st     └─────────────────────────────────────────────────────
554  
src  
typ  
doc  
txt  
par  
pid  
st   
555  end canonically_ordered_semiring
556  
557  section linear_ordered_semiring
558  variable [linear_ordered_semiring α]
id             └─────────────────────┘
src            └─────────────────────┘
typ            └─────────────────────┘
559  
560  theorem pow_pos {a : α} (H : 0 < a) : ∀ (n : ℕ), 0 < a ^ n
id                                                    
src                                                      
typ                                                   
561  | 0     := zero_lt_one
id              └─────────┘
src             └─────────┘
typ             └─────────┘
562  | (n+1) := mul_pos H (pow_pos _)
id             └─────┘   └─────┘
src            └─────┘
typ            └─────┘   └─────┘
563  
564  theorem pow_nonneg {a : α} (H : 0 ≤ a) : ∀ (n : ℕ), 0 ≤ a ^ n
id                                                       
src                                                         
typ                                                      
565  | 0     := zero_le_one
id              └─────────┘
src             └─────────┘
typ             └─────────┘
566  | (n+1) := mul_nonneg H (pow_nonneg _)
id             └────────┘   └────────┘
src            └────────┘
typ            └────────┘   └────────┘
567  
568  theorem pow_lt_pow_of_lt_left {x y : α} {n : ℕ} (Hxy : x < y) (Hxpos : 0 ≤ x) (Hnpos : 0 < n) : x ^ n < y ^ n :=
id                                                                                                
src                                                                                                      
typ                                                                                               
569  begin
st   └─────
570    cases lt_or_eq_of_le Hxpos,
id           └────────────┘ └───┘
src    └────┘└────────────┘
typ    └────┘└────────────┘└───┘
doc    └────┘              
txt    └────┘              
par    └────┘              
pid                       
st   ───────────────────────────┘└─
571    { rw ←nat.sub_add_cancel Hnpos,
id           └────────────────┘ └───┘
src      └──┘└────────────────┘
typ      └──┘└────────────────┘└───┘
doc      └──┘                  
txt      └──┘                  
par      └──┘                  
pid        └┘                  
st   ───┘└──────────────────────────┘└─
572      induction (n - 1), { simpa only [pow_one] },
id                                      └─────┘
src      └────────┘  └─┘    └──────────┘└─────┘└┘
typ      └────────┘ └─┘    └──────────┘└─────┘└┘
doc      └────────┘   └─┘    └──────────┘       └┘
txt      └────────┘   └─┘    └──────────┘       └┘
par      └────────┘   └─┘    └──────────┘       └┘
pid                  └─┘         └──┘└┘       
st   ────────────────────┘└──┘└───────────────────┘└┘
573      rw [pow_add, pow_add, nat.succ_eq_add_one, pow_one, pow_one],
id           └─────┘  └─────┘  └─────────────────┘  └─────┘  └─────┘
src      └──┘└─────┘└┘└─────┘└┘└─────────────────┘└┘└─────┘└┘└─────┘
typ      └──┘└─────┘└┘└─────┘└┘└─────────────────┘└┘└─────┘└┘└─────┘
doc      └──┘       └┘       └┘                   └┘       └┘       
txt      └──┘       └┘       └┘                   └┘       └┘       
par      └──┘       └┘       └┘                   └┘       └┘       
pid        └┘       └┘       └┘                   └┘       └┘       
st   ──────────────┘└───────┘└───────────────────┘└───────┘└───────┘└─
574      apply mul_lt_mul ih (le_of_lt Hxy) h (le_of_lt (pow_pos (lt_trans h Hxy) _)) },
id             └────────┘ └┘                   └──────┘  └─────┘  └──────┘  └─┘
src      └────┘└────────┘              └┘  └──────┘ └─────┘ └──────┘    └────┘
typ      └────┘└────────┘└┘            └┘  └──────┘ └─────┘ └──────┘└─┘└────┘
doc      └────┘                        └┘                               └────┘
txt      └────┘                        └┘                               └────┘
par      └────┘                        └┘                               └────┘
pid                                   └┘                               └───┘
st   ────────────────────────────────────────────────────────────────────────────────┘└┘
575    { rw [←h, zero_pow Hnpos], apply pow_pos (by rwa ←h at Hxy : 0 < y),}
id              └──────┘ └───┘         └─────┘                       
src      └───┘ └┘└──────┘       └────┘└─────┘   └───┘ └──────┘└──┘ 
typ      └───┘└┘└──────┘└───┘  └────┘└─────┘   └───┘└──────┘└──┘
doc      └───┘ └┘               └────┘          └───┘ └──────┘└──┘  
txt      └───┘ └┘               └────┘          └───┘ └──────┘└──┘  
par      └───┘ └┘               └────┘          └───┘ └──────┘└──┘  
pid        └─┘ └┘                              └────┘ └──────────┘  
st   ─────────┘└──────────────┘└─────────────────┘└─────────────┘└──────┘└──
576  end
st   ──┘
577  
578  theorem pow_right_inj {x y : α} {n : ℕ} (Hxpos : 0 ≤ x) (Hypos : 0 ≤ y) (Hnpos : 0 < n) (Hxyn : x ^ n = y ^ n) : x = y :=
id                                                                                                       
src                                                                                                              
typ                                                                                                      
579  begin
st   └─────
580    rcases lt_trichotomy x y with hxy | rfl | hyx,
id            └───────────┘  
src    └─────┘└───────────┘  └───────────────────┘
typ    └─────┘└───────────┘└───────────────────┘
doc    └─────┘               └───────────────────┘
txt    └─────┘               └───────────────────┘
par    └─────┘               └───────────────────┘
pid                         └───────────────────┘
st   ──────────────────────────────────────────────┘└─
581    { exact absurd Hxyn (ne_of_lt (pow_lt_pow_of_lt_left hxy Hxpos Hnpos)) },
id             └────┘ └──┘  └──────┘  └───────────────────┘ └─┘ └───┘ └───┘
src      └────┘└────┘     └──────┘ └───────────────────┘             └─┘
typ      └────┘└────┘└──┘ └──────┘ └───────────────────┘└─┘└───┘└───┘└─┘
doc      └────┘                                                      └─┘
txt      └────┘                                                      └─┘
par      └────┘                                                      └─┘
pid                                                                 └┘
st   ───┘└───────────────────────────────────────────────────────────────────┘└┘
582    { refl },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
583    { exact absurd Hxyn (ne_of_gt (pow_lt_pow_of_lt_left hyx Hypos Hnpos)) },
id             └────┘ └──┘  └──────┘  └───────────────────┘ └─┘ └───┘ └───┘
src      └────┘└────┘     └──────┘ └───────────────────┘             └─┘
typ      └────┘└────┘└──┘ └──────┘ └───────────────────┘└─┘└───┘└───┘└─┘
doc      └────┘                                                      └─┘
txt      └────┘                                                      └─┘
par      └────┘                                                      └─┘
pid                                                                 └┘
st   ────────────────────────────────────────────────────────────────────────┘└──
584  end
st   ──┘
585  
586  theorem one_le_pow_of_one_le {a : α} (H : 1 ≤ a) : ∀ (n : ℕ), 1 ≤ a ^ n
id                                                                 
src                                                                   
typ                                                                
587  | 0     := le_refl _
id              └─────┘
src             └─────┘
typ             └─────┘
588  | (n+1) := by simpa only [mul_one] using mul_le_mul H (one_le_pow_of_one_le n)
id                            └─────┘        └────────┘    └──────────────────┘ 
src               └──────────┘└─────┘└──────┘└────────┘                       └─
typ               └──────────┘└─────┘└──────┘└────────┘  └──────────────────┘└─
doc                └──────────┘       └──────┘                                 └─
txt                └──────────┘       └──────┘                                 └─
par                └──────────┘       └──────┘                                 └─
pid                     └──┘└┘       └────┘                                 └─
st                └─────────────────────────────────────────────────────────────────
589      zero_le_one (le_trans zero_le_one H)
id                    └──────┘ └─────────┘ 
src  ───┘            └──────┘└─────────┘ └─
typ  ───┘            └──────┘└─────────┘└─
doc  ───┘                                └─
txt  ───┘                                └─
par  ───┘                                └─
pid  ───┘                                
st   ─────────────────────────────────────────
590  
src  
typ  
doc  
txt  
par  
pid  
st   
591  /-- Bernoulli's inequality. This version works for semirings but requires
592  an additional hypothesis `0 ≤ a * a`. -/
593  theorem one_add_mul_le_pow' {a : α} (Hsqr : 0 ≤ a * a) (H : 0 ≤ 1 + a) :
id                                                                
src                                                                 
typ                                                               
594    ∀ (n : ℕ), 1 + n • a ≤ (1 + a) ^ n
id                            
src                              
typ                           
595  | 0     := le_of_eq $ add_zero _
id              └──────┘   └──────┘
src             └──────┘   └──────┘
typ             └──────┘   └──────┘
596  | (n+1) :=
id      
src      
typ     
597  calc 1 + (n + 1) • a ≤ (1 + a) * (1 + n • a) :
id                                    
src                                    
typ                                   
598    by simpa [succ_smul, mul_add, add_mul, add_monoid.mul_smul_left]
id               └───────┘  └─────┘  └─────┘  └──────────────────────┘
src       └─────┘└───────┘└┘└─────┘└┘└─────┘└┘└──────────────────────┘└─
typ       └─────┘└───────┘└┘└─────┘└┘└─────┘└┘└──────────────────────┘└─
doc       └─────┘         └┘       └┘       └┘                        └─
txt       └─────┘         └┘       └┘       └┘                        └─
par       └─────┘         └┘       └┘       └┘                        └─
pid                     └┘       └┘       └┘                        
st       └──────────────────────────────────────────────────────────────
599      using add_monoid.smul_nonneg Hsqr n
id             └────────────────────┘ └──┘ 
src  ─────────┘└────────────────────┘     
typ  ─────────┘└────────────────────┘└──┘
doc  ─────────┘                           
txt  ─────────┘                           
par  ─────────┘                           
pid  ───┘└────┘                           
st   ───────────────────────────────────────┘
600  ... ≤ (1 + a)^(n+1) : mul_le_mul_of_nonneg_left (one_add_mul_le_pow' n) H
id                     └───────────────────────┘  └─────────────────┘    
src                     └───────────────────────┘
typ                    └───────────────────────┘  └─────────────────┘    
601  
602  theorem pow_le_pow {a : α} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
id                                                                  
src                                                                       
typ                                                                 
603  let ⟨k, hk⟩ := nat.le.dest h in
id   └─┘           └─────────┘ 
src                 └─────────┘
typ  └─┘           └─────────┘ 
604  calc a ^ n = a ^ n * 1 : (mul_one _).symm
id                      └─────┘   └──┘
src                         └─────┘   └──┘
typ                     └─────┘   └──┘
605    ... ≤ a ^ n * a ^ k : mul_le_mul_of_nonneg_left
id                     └───────────────────────┘
src                       └───────────────────────┘
typ                    └───────────────────────┘
606      (one_le_pow_of_one_le ha _)
id        └──────────────────┘ └┘
src       └──────────────────┘
typ       └──────────────────┘ └┘
607      (pow_nonneg (le_trans zero_le_one ha) _)
id        └────────┘  └──────┘ └─────────┘ └┘
src       └────────┘  └──────┘ └─────────┘
typ       └────────┘  └──────┘ └─────────┘ └┘
608    ... = a ^ m : by rw [←hk, pow_add]
id                        └┘  └─────┘
src                    └───┘  └┘└─────┘└─
typ                  └───┘└┘└┘└─────┘└─
doc                     └───┘  └┘       └─
txt                     └───┘  └┘       └─
par                     └───┘  └┘       └─
pid                       └─┘  └┘       
st                     └──────┘└───────┘
609  
src  
typ  
doc  
txt  
par  
pid  
st   
610  lemma pow_lt_pow {a : α} {n m : ℕ} (h : 1 < a) (h2 : n < m) : a ^ n < a ^ m :=
id                                                                
src                                                                     
typ                                                               
611  begin
st   └─────
612    have h' : 1 ≤ a := le_of_lt h,
id                      └──────┘ 
src    └──────────┘ └──┘└──────┘
typ    └──────────┘└──┘└──────┘
doc    └──────────┘  └──┘        
txt    └──────────┘  └──┘        
par    └──────────┘  └──┘        
pid    └─────┘└───┘  └──┘        
st   ──────────────────────────────┘└─
613    have h'' : 0 < a := lt_trans zero_lt_one h,
id                       └──────┘ └─────────┘ 
src    └───────────┘ └──┘└──────┘└─────────┘
typ    └───────────┘└──┘└──────┘└─────────┘
doc    └───────────┘  └──┘                   
txt    └───────────┘  └──┘                   
par    └───────────┘  └──┘                   
pid    └──────┘└───┘  └──┘                   
st   ───────────────────────────────────────────┘└─
614    cases m, cases h2, rw [pow_succ, ←one_mul (a ^ n)],
id                   └┘      └──────┘   └─────┘    
src    └────┘   └────┘    └──┘└──────┘└─┘└─────┘   └┘
typ    └────┘  └────┘└┘  └──┘└──────┘└─┘└─────┘ └┘
doc    └────┘   └────┘    └──┘        └─┘           └┘
txt    └────┘   └────┘    └──┘        └─┘           └┘
par    └────┘   └────┘    └──┘        └─┘           └┘
pid                       └┘        └─┘           └┘
st   ────────┘└────────┘└────────────┘└────────────────┘└─
615    exact mul_lt_mul h (pow_le_pow h' (nat.le_of_lt_succ h2)) (pow_pos h'' _) (le_of_lt h'')
id           └────────┘   └────────┘ └┘  └───────────────┘ └┘    └─────┘         └──────┘ └─┘
src    └────┘└────────┘  └────────┘   └───────────────┘  └─┘ └─────┘   └──┘ └──────┘   └┘
typ    └────┘└────────┘ └────────┘└┘ └───────────────┘└┘└─┘ └─────┘   └──┘ └──────┘└─┘└┘
doc    └────┘                                            └─┘           └──┘            └┘
txt    └────┘                                            └─┘           └──┘            └┘
par    └────┘                                            └─┘           └──┘            └┘
pid                                                     └─┘           └──┘            
st   ──────────────────────────────────────────────────────────────────────────────────────────┘
616  end
st   └─┘
617  
618  lemma pow_le_pow_of_le_left {a b : α} (ha : 0 ≤ a) (hab : a ≤ b) : ∀ i : ℕ, a^i ≤ b^i
id                                                                         
src                                                                                
typ                                                                        
619  | 0     := by simp
src                └───┘
typ                └───┘
doc                └───┘
txt                └───┘
par                └───┘
pid                    
st                └────┘
620  | (k+1) := mul_le_mul hab (pow_le_pow_of_le_left _) (pow_nonneg ha _) (le_trans ha hab)
id             └────────┘ └─┘  └───────────────────┘     └────────┘ └┘     └──────┘ └┘ └─┘
src            └────────┘                                └────────┘        └──────┘
typ            └────────┘ └─┘  └───────────────────┘     └────────┘ └┘     └──────┘ └┘ └─┘
621  
622  lemma lt_of_pow_lt_pow {a b : α} (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b :=
id                                                                      
src                                                                           
typ                                                                     
623  lt_of_not_ge $ λ hn, not_lt_of_ge (pow_le_pow_of_le_left hb hn _) h
id   └──────────┘     └┘  └──────────┘  └───────────────────┘ └┘ └┘    
src  └──────────┘         └──────────┘  └───────────────────┘
typ  └──────────┘     └┘  └──────────┘  └───────────────────┘ └┘ └┘    
624  
625  private lemma pow_lt_pow_of_lt_one_aux {a : α} (h : 0 < a) (ha : a < 1) (i : ℕ) :
id                                                                           
src                                                                             
typ                                                                          
626    ∀ k : ℕ, a ^ (i + k + 1) < a ^ i
id                         
src                            
typ                        
627  | 0 := begin simp only [add_zero], rw ←one_mul (a^i), exact mul_lt_mul ha (le_refl _) (pow_pos h _) zero_le_one end
id                           └──────┘       └─────┘           └────────┘ └┘  └─────┘     └─────┘     └─────────┘
src               └─────────┘└──────┘  └──┘└─────┘     └────┘└────────┘   └─────┘└──┘ └─────┘ └──┘└─────────┘
typ               └─────────┘└──────┘  └──┘└─────┘   └────┘└────────┘└┘ └─────┘└──┘ └─────┘└──┘└─────────┘
doc               └─────────┘          └──┘             └────┘                    └──┘         └──┘           
txt               └─────────┘          └──┘             └────┘                    └──┘         └──┘           
par               └─────────┘          └──┘             └────┘                    └──┘         └──┘           
pid                   └──┘└┘            └┘                                      └──┘         └──┘           
st          └────────────────────────┘└─────────────────┘└──────────────────────────────────────────────────────────┘└─┘
628  | (k+1) :=
id       
src      
typ      
629    begin
st     └─────
630      rw ←one_mul (a^i),
id           └─────┘   
src      └──┘└─────┘    
typ      └──┘└─────┘  
doc      └──┘           
txt      └──┘           
par      └──┘           
pid        └┘           
st   ────────────────────┘└─
631      apply mul_lt_mul ha _ _ zero_le_one,
id             └────────┘ └┘     └─────────┘
src      └────┘└────────┘  └───┘└─────────┘
typ      └────┘└────────┘└┘└───┘└─────────┘
doc      └────┘            └───┘
txt      └────┘            └───┘
par      └────┘            └───┘
pid                       └───┘
st   ──────────────────────────────────────┘└─
632      { apply le_of_lt, apply pow_lt_pow_of_lt_one_aux },
id               └──────┘
src        └────┘└──────┘  └────┘                        
typ        └────┘└──────┘  └────┘                        
doc        └────┘          └────┘                        
txt        └────┘          └────┘                        
par        └────┘          └────┘                        
pid                                                    
st   ─────┘└────────────┘└───────────────────────────────┘└┘
633      { show 0 < a ^ (i + (k + 1) + 0), apply pow_pos h }
id                                          └─────┘ 
src        └─────┘       └──┘ └─┘  └────┘└─────┘ 
typ        └─────┘    └──┘ └─┘  └────┘└─────┘
doc        └─────┘         └──┘ └─┘  └────┘        
txt        └─────┘         └──┘ └─┘  └────┘        
par        └─────┘         └──┘ └─┘  └────┘        
pid        └─────┘         └──┘ └─┘               
st   ───────────────────────────────────┘└────────────────┘└─
634    end
st   ────┘
635  
636  private lemma pow_le_pow_of_le_one_aux {a : α}  (h : 0 ≤ a) (ha : a ≤ 1) (i : ℕ) :
id                                                                            
src                                                                              
typ                                                                           
637    ∀ k : ℕ, a ^ (i + k) ≤ a ^ i
id                      
src                         
typ                     
638  | 0 := by simp
src            └───┘
typ            └───┘
doc            └───┘
txt            └───┘
par            └───┘
pid                
st            └────┘
639  | (k+1) := by rw [←add_assoc, ←one_mul (a^i)];
id                     └───────┘   └─────┘  
src               └───┘└───────┘└─┘└─────┘   └┘
typ               └───┘└───────┘└─┘└─────┘ └┘
doc                └───┘         └─┘           └┘
txt                └───┘         └─┘           └┘
par                └───┘         └─┘           └┘
pid                  └─┘         └─┘           └┘
st                └─────────────┘└──────────────┘└─
640                exact mul_le_mul ha (pow_le_pow_of_le_one_aux _) (pow_nonneg h _) zero_le_one
id                       └────────┘ └┘  └──────────────────────┘     └────────┘     └─────────┘
src                └────┘└────────┘                           └──┘ └────────┘ └──┘└─────────┘
typ                └────┘└────────┘└┘ └──────────────────────┘└──┘ └────────┘└──┘└─────────┘
doc                └────┘                                     └──┘            └──┘           
txt                └────┘                                     └──┘            └──┘           
par                └────┘                                     └──┘            └──┘           
pid                                                          └──┘            └──┘           
st   ────────────────────────────────────────────────────────────────────────────────────────────
641  
src  
typ  
doc  
txt  
par  
pid  
st   
642  lemma pow_lt_pow_of_lt_one  {a : α} (h : 0 < a) (ha : a < 1)
id                                                       
src                                                         
typ                                                      
643    {i j : ℕ} (hij : i < j) : a ^ j < a ^ i :=
id                                 
src                                    
typ                                
644  let ⟨k, hk⟩ := nat.exists_eq_add_of_lt hij in
id   └─┘            └─────────────────────┘ └─┘
src                 └─────────────────────┘
typ  └─┘            └─────────────────────┘ └─┘
645  by rw hk; exact pow_lt_pow_of_lt_one_aux h ha _ _
id         └┘        └──────────────────────┘  └┘
src     └─┘    └────┘└──────────────────────┘   └────
typ     └─┘└┘  └────┘└──────────────────────┘└┘└────
doc     └─┘    └────┘                           └────
txt     └─┘    └────┘                           └────
par     └─┘    └────┘                           └────
pid                                           └──┘
st     └───────────────────────────────────────────────
646  
src  
typ  
doc  
txt  
par  
pid  
st   
647  lemma pow_le_pow_of_le_one  {a : α} (h : 0 ≤ a) (ha : a ≤ 1)
id                                                       
src                                                         
typ                                                      
648    {i j : ℕ} (hij : i ≤ j) : a ^ j ≤ a ^ i :=
id                                 
src                                    
typ                                
649  let ⟨k, hk⟩ := nat.exists_eq_add_of_le hij in
id   └─┘            └─────────────────────┘ └─┘
src                 └─────────────────────┘
typ  └─┘            └─────────────────────┘ └─┘
650  by rw hk; exact pow_le_pow_of_le_one_aux h ha _ _
id         └┘        └──────────────────────┘  └┘
src     └─┘    └────┘└──────────────────────┘   └────
typ     └─┘└┘  └────┘└──────────────────────┘└┘└────
doc     └─┘    └────┘                           └────
txt     └─┘    └────┘                           └────
par     └─┘    └────┘                           └────
pid                                           └──┘
st     └───────────────────────────────────────────────
651  
src  
typ  
doc  
txt  
par  
pid  
st   
652  lemma pow_le_one {x : α} : ∀ (n : ℕ) (h0 : 0 ≤ x) (h1 : x ≤ 1), x ^ n ≤ 1
id                                                               
src                                                                    
typ                                                              
653  | 0     h0 h1 := le_refl (1 : α)
id                    └─────┘      
src                   └─────┘
typ                   └─────┘      
654  | (n+1) h0 h1 := mul_le_one h1 (pow_nonneg h0 _) (pow_le_one n h0 h1)
id         └┘ └┘    └────────┘     └────────┘        └────────┘
src                  └────────┘     └────────┘
typ        └┘ └┘    └────────┘     └────────┘        └────────┘
655  
656  end linear_ordered_semiring
657  
658  theorem pow_two_nonneg [linear_ordered_ring α] (a : α) : 0 ≤ a ^ 2 :=
id                           └─────────────────┘                
src                          └─────────────────┘                   
typ                          └─────────────────┘                
659  by { rw pow_two, exact mul_self_nonneg _ }
id           └─────┘        └─────────────┘
src       └─┘└─────┘  └────┘└─────────────┘└─┘
typ       └─┘└─────┘  └────┘└─────────────┘└─┘
doc       └─┘         └────┘               └─┘
txt       └─┘         └────┘               └─┘
par       └─┘         └────┘               └─┘
pid                                      └┘
st     └───────────┘└────────────────────────┘└┘
660  
661  /-- Bernoulli's inequality for `n : ℕ`, `-2 ≤ a`. -/
662  theorem one_add_mul_le_pow [linear_ordered_ring α] {a : α} (H : -2 ≤ a) :
id                               └─────────────────┘                  
src                              └─────────────────┘                   
typ                              └─────────────────┘                  
663    ∀ (n : ℕ), 1 + n • a ≤ (1 + a) ^ n
id                            
src                              
typ                           
664  | 0     := le_of_eq $ add_zero _
id              └──────┘   └──────┘
src             └──────┘   └──────┘
typ             └──────┘   └──────┘
665  | 1     := by simp
src                └───┘
typ                └───┘
doc                └───┘
txt                └───┘
par                └───┘
pid                    
st                └────┘
666  | (n+2) :=
id      
src      
typ     
667  have H' : 0 ≤ 2 + a,
id                   
src                 
typ                  
668    from neg_le_iff_add_nonneg.1 H,
id          └───────────────────┘  
src         └───────────────────┘
typ         └───────────────────┘  
669  have 0 ≤ n • (a * a * (2 + a)) + a * a,
id                             
src                               
typ                            
670    from add_nonneg (add_monoid.smul_nonneg (mul_nonneg (mul_self_nonneg a) H') n)
id          └────────┘  └────────────────────┘  └────────┘  └─────────────┘   └┘
src         └────────┘  └────────────────────┘  └────────┘  └─────────────┘
typ         └────────┘  └────────────────────┘  └────────┘  └─────────────┘   └┘
671      (mul_self_nonneg a),
id        └─────────────┘ 
src       └─────────────┘
typ       └─────────────┘ 
672  calc 1 + (n + 2) • a ≤ 1 + (n + 2) • a + (n • (a * a * (2 + a)) + a * a) :
id                                                      
src                                                          
typ                                                     
673    (le_add_iff_nonneg_right _).2 this
id      └─────────────────────┘     └──┘
src     └─────────────────────┘   
typ     └─────────────────────┘     └──┘
674  ... = (1 + a) * (1 + a) * (1 + n • a) :
id                              
src                              
typ                             
675    by { simp only [add_mul, mul_add, mul_two, mul_one, one_mul, succ_smul, add_monoid.smul_add,
id                     └─────┘  └─────┘  └─────┘  └─────┘  └─────┘  └───────┘  └─────────────────┘
src         └─────────┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└┘└───────┘└┘└─────────────────┘└─
typ         └─────────┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└┘└─────┘└┘└───────┘└┘└─────────────────┘└─
doc         └─────────┘       └┘       └┘       └┘       └┘       └┘         └┘                   └─
txt         └─────────┘       └┘       └┘       └┘       └┘       └┘         └┘                   └─
par         └─────────┘       └┘       └┘       └┘       └┘       └┘         └┘                   └─
pid             └──┘└┘       └┘       └┘       └┘       └┘       └┘         └┘                   └─
st       └──────────────────────────────────────────────────────────────────────────────────────────
676           add_monoid.mul_smul_assoc, (add_monoid.mul_smul_left _ _ _).symm],
id            └───────────────────────┘   └──────────────────────┘
src  ────────┘└───────────────────────┘└┘ └──────────────────────┘└───────────┘
typ  ────────┘└───────────────────────┘└┘ └──────────────────────┘└───────────┘
doc  ────────┘                         └┘                         └───────────┘
txt  ────────┘                         └┘                         └───────────┘
par  ────────┘                         └┘                         └───────────┘
pid  ────────┘                         └┘                         └───────────┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
677         ac_refl }
src         └──────┘
typ         └──────┘
doc         └──────┘
txt         └──────┘
par         └──────┘
pid                
st   ──────────────┘└┘
678  ... ≤ (1 + a) * (1 + a) * (1 + a)^n :
id                            
src                              
typ                           
679    mul_le_mul_of_nonneg_left (one_add_mul_le_pow n) (mul_self_nonneg (1 + a))
id     └───────────────────────┘  └────────────────┘     └─────────────┘     
src    └───────────────────────┘                         └─────────────┘    
typ    └───────────────────────┘  └────────────────┘     └─────────────┘     
680  ... = (1 + a)^(n + 2) : by simp only [pow_succ, mul_assoc]
id                                     └──────┘  └───────┘
src                          └─────────┘└──────┘└┘└───────┘└─
typ                         └─────────┘└──────┘└┘└───────┘└─
doc                             └─────────┘        └┘         └─
txt                             └─────────┘        └┘         └─
par                             └─────────┘        └┘         └─
pid                                 └──┘└┘        └┘         
st                             └────────────────────────────────
681  
src  
typ  
doc  
txt  
par  
pid  
st   
682  /-- Bernoulli's inequality reformulated to estimate `a^n`. -/
683  theorem one_add_sub_mul_le_pow [linear_ordered_ring α]
id                                   └─────────────────┘ 
src                                  └─────────────────┘
typ                                  └─────────────────┘ 
684    {a : α} (H : -1 ≤ a) (n : ℕ) : 1 + n • (a - 1) ≤ a ^ n :=
id                                             
src                                                
typ                                            
685  have -2 ≤ a - 1, by { rw [bit0, neg_add], exact sub_le_sub_right H 1 },
id                         └──┘  └─────┘         └──────────────┘ 
src                     └──┘└──┘└┘└─────┘  └────┘└──────────────┘ └─┘
typ                    └──┘└──┘└┘└─────┘  └────┘└──────────────┘└─┘
doc                        └──┘    └┘         └────┘                 └─┘
txt                        └──┘    └┘         └────┘                 └─┘
par                        └──┘    └┘         └────┘                 └─┘
pid                          └┘    └┘                               └┘
st                      └─────────┘└───────┘└────────────────────────────┘└┘
686  by simpa only [add_sub_cancel'_right] using one_add_mul_le_pow this n
id                  └───────────────────┘        └────────────────┘ └──┘ 
src     └──────────┘└───────────────────┘└──────┘└────────────────┘     
typ     └──────────┘└───────────────────┘└──────┘└────────────────┘└──┘
doc     └──────────┘                     └──────┘└────────────────┘     
txt     └──────────┘                     └──────┘                       
par     └──────────┘                     └──────┘                       
pid          └──┘└┘                     └────┘                       
st     └───────────────────────────────────────────────────────────────────
687  
src  
typ  
doc  
txt  
par  
pid  
st   
688  namespace int
689  
690  lemma units_pow_two (u : units ℤ) : u ^ 2 = 1 :=
id                            └───┘         
src                           └───┘          
typ                           └───┘         
691  (units_eq_one_or u).elim (λ h, h.symm ▸ rfl) (λ h, h.symm ▸ rfl)
id    └─────────────┘  └──┘       └───┘  └─┘       └───┘  └─┘
src   └─────────────┘   └──┘         └───┘  └─┘         └───┘  └─┘
typ   └─────────────┘  └──┘       └───┘  └─┘       └───┘  └─┘
692  
693  lemma units_pow_eq_pow_mod_two (u : units ℤ) (n : ℕ) : u ^ n = u ^ (n % 2) :=
id                                       └───┘                    
src                                      └───┘                        
typ                                      └───┘                    
694  by conv {to_lhs, rw ← nat.mod_add_div n 2}; rw [pow_add, pow_mul, units_pow_two, one_pow, mul_one]
id                         └─────────────┘          └─────┘  └─────┘  └───────────┘  └─────┘  └─────┘
src     └────┘└────┘└┘└───┘└─────────────┘ └┘  └──┘└─────┘└┘└─────┘└┘└───────────┘└┘└─────┘└┘└─────┘└─
typ     └────┘└────┘└┘└───┘└─────────────┘└┘  └──┘└─────┘└┘└─────┘└┘└───────────┘└┘└─────┘└┘└─────┘└─
doc                                              └──┘       └┘       └┘             └┘       └┘       └─
txt     └────┘└────┘└┘└───┘                └┘  └──┘       └┘       └┘             └┘       └┘       └─
par     └────┘└────┘└┘└───┘                └┘  └──┘       └┘       └┘             └┘       └┘       └─
pid         └────────────┘                └─┘    └┘       └┘       └┘             └┘       └┘       
st     └─────┘└────┘└────────────────────────┘└┘└───┘└─────┘└───────┘└─────────────┘└───────┘└───────┘
695  
src  
typ  
doc  
txt  
par  
pid  
st   
696  end int
697  
698  @[simp] lemma neg_square {α} [ring α] (z : α) : (-z)^2 = z^2 :=
id                                 └──┘                 
src                                └──┘                     
typ                                └──┘                 
doc    └──┘
699  by simp [pow, monoid.pow]
id                 └────────┘
src     └────┘   └┘└────────┘└─
typ     └────┘   └┘└────────┘└─
doc     └────┘   └┘└────────┘└─
txt     └────┘   └┘          └─
par     └────┘   └┘          └─
pid            └┘          
st     └───────────────────────
700  
src  
typ  
doc  
txt  
par  
pid  
st   
701  lemma div_sq_cancel {α} [field α] {a : α} (ha : a ≠ 0) (b : α) : a^2 * b / a = a * b :=
id                            └───┘                                       
src                           └───┘                                              
typ                           └───┘                                       
702  by rw [pow_two, mul_assoc, mul_div_cancel_left _ ha]
id          └─────┘  └───────┘  └─────────────────┘   └┘
src     └──┘└─────┘└┘└───────┘└┘└─────────────────┘└─┘  
typ     └──┘└─────┘└┘└───────┘└┘└─────────────────┘└─┘└┘
doc     └──┘       └┘         └┘                   └─┘  
txt     └──┘       └┘         └┘                   └─┘  
par     └──┘       └┘         └┘                   └─┘  
pid       └┘       └┘         └┘                   └─┘  
st     └──────────┘└─────────┘└────────────────────────┘